--- /dev/null
+(*#* #stop file *)
+
+Require Export terms_defs.
+
+ Inductive Set C := CSort : nat -> C
+ | CTail : C -> K -> T -> C.
+
+ Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
+
+ Definition r: K -> nat -> nat := [k;i] Cases k of
+ | (Bind _) => i
+ | (Flat _) => (S i)
+ end.
+
+ Fixpoint app [c:C] : nat -> T -> T := [j;t]Cases j c of
+ | (0) _ => t
+ | _ (CSort _) => t
+ | (S i) (CTail c k u) => (app c (r k i) (TTail k u t))
+ end.
+
+ Section r_props. (********************************************************)
+
+ Theorem r_S: (k:?; i:?) (r k (S i)) = (S (r k i)).
+ XElim k; XAuto.
+ Qed.
+
+ Theorem r_plus_sym: (k:?; i,j:?) (r k (plus i j)) = (plus i (r k j)).
+ XElim k; Intros; Simpl; XAuto.
+ Qed.
+
+ Theorem r_minus: (i,n:?) (lt n i) ->
+ (k:?) (minus (r k i) (S n)) = (r k (minus i (S n))).
+ XElim k; Intros; Simpl; XEAuto.
+ Qed.
+
+ Theorem r_dis: (k:?; P:Prop)
+ (((i:?) (r k i) = i) -> P) ->
+ (((i:?) (r k i) = (S i)) -> P) -> P.
+ XElim k; XAuto.
+ Qed.
+
+ End r_props.
+
+ Tactic Definition RRw :=
+ Repeat (Rewrite r_S Orelse Rewrite r_plus_sym).
+
+ Section r_arith. (********************************************************)
+
+ Theorem r_arith0: (k:?; i:?) (minus (r k (S i)) (1)) = (r k i).
+ Intros; RRw; Rewrite minus_Sx_SO; XAuto.
+ Qed.
+
+ Theorem r_arith1: (k:?; i,j:?) (minus (r k (S i)) (S j)) = (minus (r k i) j).
+ Intros; RRw; XAuto.
+ Qed.
+
+ End r_arith.
+
+ Section app_props. (******************************************************)
+
+ 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.
+ XElim c; XAuto.
+ Qed.
+
+ End app_props.
+
+ Hints Resolve app_csort app_O : ltlc.