proposition: Lemma presubst_singleton_conv_sim M M' T T' Q R R' : envSub Q 0 0 -> conv_term M M' Q -> T ~(Q) T' -> conv_term R R' Q -> presubst M {x/T} = R -> presubst M' {x/T'} = R'.
proof: Proof. intros. unfold presubst. change {x/T'} with (copy 0 None ++ {x/T'}). apply presubst_singleton_conv_sim_aux with M T Q R; trivial. intros; destruct j; trivial. lia. rewrite !lift_0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)