proposition: Lemma conv_term_lower : forall M k (M0: env M |= k :!), conv_term (term M) (prelower_aux (term M) k) (lowerEnvSubst k (length (env M))).
proof: Proof. destruct M as [E Pt T M]; induction M; intros k M0; simpl. unfold prelower_aux; simpl in * . assert (hint: k = x -> False). intros; apply varD_UD_absurd with E x A; trivial. rewrite <- H; trivial. destruct (le_gt_dec k x); constructor; simpl; split; solve [ apply nth_some with (Some A); trivial | destruct (eq_nat_dec k x); destruct (le_gt_dec k x); solve [try_solve | lia] ]. constructor 2. constructor 3. rewrite (lift_lowerEnvSubst k (length E)); try_solve. constructor 4. apply IHM1; trivial. apply IHM2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)