diff options
Diffstat (limited to 'test-suite/success/autointros.v')
-rw-r--r-- | test-suite/success/autointros.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v new file mode 100644 index 00000000..0a081271 --- /dev/null +++ b/test-suite/success/autointros.v @@ -0,0 +1,15 @@ +Set Automatic Introduction. + +Inductive even : nat -> Prop := +| even_0 : even 0 +| even_odd : forall n, odd n -> even (S n) +with odd : nat -> Prop := +| odd_1 : odd 1 +| odd_even : forall n, even n -> odd (S n). + +Lemma foo {n : nat} (E : even n) : even (S (S n)) +with bar {n : nat} (O : odd n) : odd (S (S n)). +Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H). + destruct O. repeat constructor. apply odd_even. apply (foo _ H). +Defined. + |