proposition: Lemma activeEnv_lower_aux : forall M n (Menv: env M |= n :!), activeEnv (proj1_sig (lower_aux M Menv)) = loweredEnv (activeEnv M) n.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. unfold loweredEnv; simpl. destruct (le_gt_dec n x); simpl. destruct (le_gt_dec x n). exfalso; apply varD_UD_absurd with E x A; trivial. replace x with n; [trivial | lia]. rewrite initialSeg_app; autorewrite with datatypes using trivial. rewrite initialSeg_copy. rewrite Nat.min_r; trivial. rewrite finalSeg_copy; [idtac | lia]. rewrite <- app_ass. rewrite <- copy_split. replace (pred x) with (n + (x - S n)); trivial. lia. rewrite initialSeg_full; autorewrite with datatypes using simpl; try lia. rewrite finalSeg_empty; autorewrite with datatypes using simpl; try lia. rewrite <- app_nil_end; trivial. destruct n; try_solve. rewrite activeEnv_abs with (buildT (TAbs M)) I. set (l := proj1_sig (lower_aux (buildT (TAbs M)) Menv)). assert (labs: isAbs l). apply abs_isAbs with A (prelower_aux Pt (S n)). unfold l; destruct (lower_aux (buildT (TAbs M)) Menv) as [W [WE [WPt WT]]]. simpl; rewrite WPt; trivial. rewrite (activeEnv_abs l labs). rewrite (lower_tail (activeEnv (absBody (M:=buildT (TAbs M)) I)) n). replace (activeEnv (absBody labs)) with (loweredEnv (activeEnv (absBody (M:=buildT (TAbs M)) I)) (S n)); trivial. change (absBody (M:=buildT (TAbs M)) I) with (buildT M). rewrite <- (IHM (S n) Menv). rewrite (@lower_absBody E Pt A B M n Menv Menv); trivial. rewrite activeEnv_app with (buildT (TApp M1 M2)) I. rewrite loweredEnv_distr_sum. set (l := proj1_sig (lower_aux (buildT (TApp M1 M2)) Menv)). assert (lapp: isApp l). apply app_isApp with (prelower_aux PtL n) (prelower_aux PtR n). unfold l; destruct (lower_aux (buildT (TApp M1 M2)) Menv) as [W [WE [WPt WT]]]. simpl; rewrite WPt; trivial. rewrite (activeEnv_app l lapp). unfold l. set (wL := lower_appBodyL Menv M1 M2 lapp); simpl in *; rewrite wL. set (wR := lower_appBodyR Menv M1 M2 lapp); simpl in *; rewrite wR. rewrite (IHM1 n). rewrite (IHM2 n); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)