proposition: Lemma lift_fold : forall Pt m n, lift Pt (m + n) = lift (lift Pt m) n.
proof: Proof. intros Pt m n. unfold lift. destruct (lift_aux (m+n) Pt 0) as [L [envL [termL typeL]]]. destruct (lift_aux m Pt 0) as [Rm [envRm [termRm typeRm]]]. simpl. destruct (lift_aux n Rm 0) as [Rn [envRn [termRn typeRn]]]. apply term_eq; simpl in * . rewrite envL, envRn, envRm. unfold liftedEnv; simpl. rewrite !finalSeg_full, Nat.add_comm, copy_split, app_ass; trivial. rewrite termL, termRn, termRm, Nat.add_comm. fold (prelift (term Pt) (n+m)). rewrite prelift_fold. trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)