proposition: Lemma lower_eq : forall M N (M0: env M |= 0 :!) (N0: env N |= 0 :!), M = N -> lower M M0 = lower N N0.
proof: Proof. intros. apply term_eq. rewrite !lower_env; rewrite H; trivial. rewrite !lower_term; rewrite H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)