proposition: Lemma activeEnv_lift_aux : forall M n k, activeEnv (proj1_sig (lift_aux n M k)) [=] liftedEnv n (activeEnv M) k.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. unfold liftedEnv; simpl. destruct (le_gt_dec k x); simpl. rewrite initialSeg_app; autorewrite with datatypes using trivial. rewrite initialSeg_copy. rewrite Nat.min_r; trivial. rewrite finalSeg_copy; trivial. rewrite <- copy_split. repeat (rewrite <- app_ass; rewrite <- copy_split). replace (x + n) with (k + n + (x - k)); [apply env_eq_refl | 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. apply env_eq_empty_tail. simpl; unfold liftedEnv. destruct k; unfold finalSeg; simpl; rewrite <- app_nil_end; change (copy n (None (A:=SimpleType))) with (EmptyEnv ++ copy n None); apply env_eq_empty_tail. rewrite activeEnv_abs with (buildT (TAbs M)) I. set (l := proj1_sig (lift_aux n (buildT (TAbs M)) k)). assert (labs: isAbs l). apply abs_isAbs with A (prelift_aux n Pt (S k)). unfold l; destruct (lift_aux n (buildT (TAbs M)) k) as [W [WE [WPt WT]]]. simpl; rewrite WPt; trivial. rewrite (activeEnv_abs l labs). rewrite (lift_tail (activeEnv (absBody (M:=buildT (TAbs M)) I)) n k). apply env_eq_tail. simpl; fold (activeEnv (buildT M)). rewrite <- (IHM n (S k)). unfold l; rewrite (lift_absBody M). apply env_eq_refl. rewrite activeEnv_app with (buildT (TApp M1 M2)) I. rewrite (liftedEnv_distr_sum (activeEnv (appBodyL (M:=buildT (TApp M1 M2)) I)) (activeEnv (appBodyR (M:=buildT (TApp M1 M2)) I)) n k). set (l := proj1_sig (lift_aux n (buildT (TApp M1 M2)) k)). assert (lapp: isApp l). apply app_isApp with (prelift_aux n PtL k) (prelift_aux n PtR k). unfold l; destruct (lift_aux n (buildT (TApp M1 M2)) k) as [W [WE [WPt WT]]]. simpl; rewrite WPt; trivial. rewrite (activeEnv_app l lapp). unfold l. rewrite (lift_appBodyL n k M1 M2 lapp). rewrite (lift_appBodyR n k M1 M2 lapp). rewrite (IHM1 n k). rewrite (IHM2 n k). apply env_eq_sum; apply env_eq_refl. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)