Require Import syntax.


Inductive F : tm → Prop :=
  | F_abs : ∀ (v : vari) (s : ty) (e : tm), F (abs v s e)
  | F_clos : ∀ (e e1 : tm) (v : vari) (s : ty), F e → F (clos e v s e1).
Inductive Sno : tm → Prop :=
  | Sno_o : Sno o
  | Sno_s : ∀ e : tm, Sno e → Sno (succ e).

Inductive NF : tm → Prop :=
  | NF_ttt : NF ttt
  | NF_fff : NF fff
  | NF_Sno : ∀ e : tm, Sno e → NF e
  | NF_F : ∀ e : tm, F e → NF e.


Definition NFsucc (e : tm) :=
  match e return Prop with
  | o ⇒
       True
      
  | ttt ⇒ True
      
  | fff ⇒ True
      
  | abs v s e ⇒ True
      
  | appl e1 e2 ⇒ True
      
  | cond e1 e2 e3 ⇒ True
      
  | var v ⇒ True
      
  | succ n ⇒ Sno (succ n)
      
  | prd n ⇒ True
      
  | is_o n ⇒ True
      
  | Fix v s e ⇒ True
      
  | clos e v s e1 ⇒ True
  end.

Goal ∀ e : tm, NF (succ e) → Sno (succ e).
intros e HNF. change (NFsucc (succ e)) in |- ×.
elim HNF; simpl in |- *; intros; exact I || elim H; simpl in |- *; intros;
 exact I || apply Sno_s; assumption.
Save inv_NF_Sno.

Definition SnoSucc (e : tm) :=
  match e return Prop with
  | o ⇒
       True
      
  | ttt ⇒ True
      
  | fff ⇒ True
      
  | abs v s e ⇒ True
      
  | appl e1 e2 ⇒ True
      
  | cond e1 e2 e3 ⇒ True
      
  | var v ⇒ True
      
  | succ n ⇒ Sno n
      
  | prd n ⇒ True
      
  | is_o n ⇒ True
      
  | Fix v s e ⇒ True
      
  | clos e v s e1 ⇒ True
  end.

Goal ∀ e : tm, Sno (succ e) → Sno e.
intros e HSno. change (SnoSucc (succ e)) in |- ×.
elim HSno; simpl in |- *; intros; exact I || assumption.
Save inv_Sno_s.