Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
+ Tactic Definition CGenBase :=
+ Match Context With
+ | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> TGenBase.
+
Definition r: K -> nat -> nat := [k;i] Cases k of
| (Bind _) => i
| (Flat _) => (S i)