proposition: Lemma presubst_disjoint : forall Pt Pt_x G, presubst (presubst Pt (lift_subst (None::G) 1)) {x/Pt_x} = presubst Pt (Some Pt_x :: lift_subst G 1).
proof: Proof. intros; unfold presubst. replace (Some Pt_x :: lift_subst G 1) with (copy 0 None ++ Some Pt_x :: lift_subst G 1). rewrite <- (presubst_aux_disjoint Pt Pt_x G 0 0). trivial. simpl; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)