proposition: Lemma conv_term_unique : forall M N N' Q, conv_term M N Q -> conv_term M N' Q -> N = N'.
proof: Proof. induction M; intros; inversion H; inversion H0. assert (y = y0); auto. apply envSub_Lok with Q x; trivial. trivial. rewrite IHM with R R0 (envSubst_lift1 Q); trivial. rewrite (IHM1 RL RL0 Q); trivial. rewrite (IHM2 RR RR0 Q); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)