proposition: Lemma conv_term_refl : forall M, conv_term (term M) (term M) (idEnvSubst (length (env M))).
proof: Proof. destruct M as [E Pt T M]; induction M; simpl. constructor 1; simpl; split; trivial. apply nth_some with (Some A); trivial. constructor 2. constructor 3; trivial. setoid_replace (envSubst_lift1 (idEnvSubst (length E))) with (idEnvSubst (S (length E))); trivial. constructor; intros i j; intros; destruct i; destruct j; simpl in *; split_all; try lia. constructor 4; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)