diff options
Diffstat (limited to 'test-suite/success/Case5.v')
-rw-r--r-- | test-suite/success/Case5.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v new file mode 100644 index 00000000..fe49cdf9 --- /dev/null +++ b/test-suite/success/Case5.v @@ -0,0 +1,14 @@ + +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. |