aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ideal-features/Case5.v
blob: d703286f900fc33a0d12a471060fd2eb7fb9cde8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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.