proposition: Lemma terms_lift_eq : forall M N, lift M 1 = lift N 1 -> M = N.
proof: Proof. intros. apply term_eq. cut (env (lift M 1) = env (lift N 1)). autorewrite with terms datatypes using unfold liftedEnv; try_solve. rewrite H; trivial. apply term_prelift_eq with 1 0. cut (term (lift M 1) = term (lift N 1)). autorewrite with terms using trivial. rewrite H; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)