proposition: Lemma prelift_prelower_aux : forall M i, env M |= i :! -> prelift_aux 1 (prelower_aux (term M) i) i = (term M).
proof: Proof. destruct M as [E Pt T M]. induction M; simpl; intros. destruct (le_gt_dec i x); simpl. destruct (le_gt_dec i (pred x)); simpl. destruct x. assert (i = 0). lia. rewrite H0 in H. inversion v; destruct E; inversion H; try_solve. assert (pred (S x) + 1 = S x); [lia | auto]. assert (i = x). lia. inversion v; destruct E; inversion H; try_solve. destruct (le_gt_dec i x); simpl; trivial. assert (i = x). lia. inversion v; destruct E; inversion H; try_solve. trivial. set (w := IHM (S i)); simpl in w. rewrite w; trivial. set (w := IHM1 i); simpl in w; rewrite w; trivial. set (t := IHM2 i); simpl in t; rewrite t; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)