diff options
Diffstat (limited to 'test-suite/ideal-features/Case5.v')
-rw-r--r-- | test-suite/ideal-features/Case5.v | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test-suite/ideal-features/Case5.v b/test-suite/ideal-features/Case5.v deleted file mode 100644 index d703286f9..000000000 --- a/test-suite/ideal-features/Case5.v +++ /dev/null @@ -1,15 +0,0 @@ - -Reset ff. -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. |