test-suite/success/Destruct.v


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. 
NewDestruct X. (* Should find axiom X and should handle arguments of X *)
Assumption.
Assumption.
Assumption.
Qed.