blob: b909e45e72bb6f76b4880de0ffba3f63b586d451 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Submitted by Robert Schneck *)
Parameter A B C D : Prop.
Axiom X : A -> B -> C /\ D.
Lemma foo : A -> B -> C.
Proof.
intros.
destruct X. (* Should find axiom X and should handle arguments of X *)
assumption.
assumption.
assumption.
Qed.
|
