Require Export terms_defs.
- Inductive Set C := CSort : nat -> C
- | CTail : C -> K -> T -> C.
+ Inductive Set C := CSort: nat -> C
+ | CTail: C -> K -> T -> C.
Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
+ Tactic Definition CGenBase :=
+ Match Context With
+ | [ H: (CSort ?) = (CSort ?) |- ? ] -> Inversion H; Clear H
+ | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> TGenBase.
+
Definition r: K -> nat -> nat := [k;i] Cases k of
| (Bind _) => i
| (Flat _) => (S i)
Section app_props. (******************************************************)
- Theorem app_csort : (t:?; i,n:?) (app (CSort n) i t) = t.
+ Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
XElim i; Intros; Simpl; XAuto.
Qed.
- Theorem app_O : (c:?; t:?) (app c (0) t) = t.
+ Theorem app_O: (c:?; t:?) (app c (0) t) = t.
XElim c; XAuto.
Qed.