helm/matita/tests/inversion.ma

   1 inductive nat : Set \def
   2    O : nat
   3  | S : nat \to nat.
   4
   5 inductive le (n:nat) : nat \to Prop \def
   6    leO : le n n
   7  | leS : \forall m. le n m \to le n (S m).
   8
   9 alias symbol "eq" (instance 0) = "leibnitz's equality".
  10
  11 theorem test_inversion: \forall n. le n O \to n=O.
  12  intros.
  13  cut O=O.
  14   (* goal 2: 0 = 0 *)
  15   goal 7. reflexivity.
  16   (* goal 1 *)
  17   generalize Hcut.      (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
  18   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  19   intro. reflexivity.
  20   simplify. intros.
  21   discriminate H3.
  22 qed.