proposition: Lemma terms_conv_activeEnv: forall M N Q, M ~(Q) N -> forall p A, activeEnv M |= p := A -> exists q, envSub Q p q.
proof: Proof. destruct M as [E Pt T M]; induction M; intros; inversion H. inversion H1; exists y. rewrite <- (@activeEnv_var_single (buildT (TVar v)) x p A0); trivial. destruct p; try_solve. term_inv N; inversion H1. set (Conv := @abs_conv_absBody_aux (buildT (TAbs M)) (buildT (TAbs T)) Q I I H). set (Mdec := varD_tail_rev (activeEnv (buildT M)) H0). destruct (IHM (buildT T) (envSubst_lift1 Q) Conv (Datatypes.S p) A0 Mdec). destruct x. destruct Q; try_solve. exists x; destruct Q; trivial. rewrite (activeEnv_app (buildT (TApp M1 M2)) I) in H0. assert (Napp: isApp N). term_inv N; inversion H1. destruct (env_sum_varDecl (activeEnv (buildT M1)) (activeEnv (buildT M2)) H0) as [[l _] | r]. set (Conv := app_conv_app_left_aux (M := buildT (TApp M1 M2)) I Napp H). exact (IHM1 (appBodyL Napp) Q Conv p A0 l). set (Conv := app_conv_app_right_aux (M := buildT (TApp M1 M2)) I Napp H). exact (IHM2 (appBodyR Napp) Q Conv p A0 r). Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)