| Flat : F -> K.
Inductive Set T := TSort : nat -> T
- | TBRef : nat -> T
+ | TLRef : nat -> T
| TTail : K -> T -> T -> T.
Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
+ Tactic Definition TGenBase :=
+ Match Context With
+ | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> Idtac.
+
Definition s: K -> nat -> nat := [k;i] Cases k of
| (Bind _) => (S i)
| (Flat _) => i