proposition: Lemma term_prelift_eq : forall M N i j, prelift_aux i M j = prelift_aux i N j -> M = N .
proof: Proof. induction M; destruct N; intros; try_solve; try solve [destruct (le_gt_dec j x); try_solve]. destruct (le_gt_dec j x); destruct (le_gt_dec j x0); try_solve. inversion H. cut (x = x0); [auto | lia]. inversion H; lia. inversion H; lia. rewrite (IHM N i (S j)); inversion H; trivial. rewrite (IHM1 N1 i j). rewrite (IHM2 N2 i j). trivial. inversion H; trivial. inversion H; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)