diff options
Diffstat (limited to 'etc/coq/multiple/c.v')
| -rw-r--r-- | etc/coq/multiple/c.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v index 490c3250..7b15abad 100644 --- a/etc/coq/multiple/c.v +++ b/etc/coq/multiple/c.v @@ -1,14 +1,14 @@ (* Simple tests for multiple file handling *) +Require d. (* d requires a *) Require a. Require b. -Goal (A,B:Prop)(and A B) -> (and B A). -Intros A B H. -Induction H. -Apply conj. -Assumption. -Assumption. +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + elim H. + intros. + split. + assumption. + assumption. Save and_comms_c. - - |