proposition: Lemma conv_env_absBody : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q, conv_term (term M) (term N) Q -> conv_env M N Q -> conv_env (absBody Mabs) (absBody Nabs) (envSubst_lift1 Q).
proof: Proof. intros. inversion H; try solve [term_inv M; term_inv N]. assert (Ecomp: env_comp_on (activeEnv (absBody Mabs)) (activeEnv (absBody Nabs)) 0). intros B C M0 N0. set (Mb := activeEnv_subset (absBody Mabs) M0). set (Nb := activeEnv_subset (absBody Nabs) N0). rewrite absBody_env in Mb. rewrite absBody_env in Nb. rewrite (abs_term M Mabs) in H1; inversion H1; rewrite <- H6 in Mb. rewrite (abs_term N Nabs) in H2; inversion H2; rewrite <- H8 in Nb. inversion Mb; inversion Nb; try_solve. intros x y xy B; split. destruct x; destruct y; try solve [destruct Q; try_solve]. set (hint := terms_conv_var_usage (absBody Mabs) (absBody Nabs) Ecomp xy). rewrite (absBody_term M Mabs (sym_eq H1)) in hint. rewrite (absBody_term N Nabs (sym_eq H2)) in hint. apply (proj1 (hint H3 B)). term_inv M; term_inv N. fold (activeEnv (buildT T)); fold (activeEnv (buildT T0)). assert (Qxy: envSub Q x y). destruct Q; trivial. intro TxA. assert (activeEnv Tr0 |= y := B). apply (proj1 (H0 x y Qxy B)); trivial. simpl; fold (activeEnv (buildT T)). apply varD_tail; trivial. apply varD_tail_rev; trivial. destruct x; destruct y; try solve [destruct Q; try_solve]. set (hint := terms_conv_var_usage (absBody Mabs) (absBody Nabs) Ecomp xy). rewrite (absBody_term M Mabs (sym_eq H1)) in hint. rewrite (absBody_term N Nabs (sym_eq H2)) in hint. apply (proj2 (hint H3 B)). term_inv M; term_inv N. fold (activeEnv (buildT T)); fold (activeEnv (buildT T0)). assert (Qxy: envSub Q x y). destruct Q; trivial. intro TxA. assert (activeEnv Tr |= x := B). apply (proj2 (H0 x y Qxy B)); trivial. simpl; fold (activeEnv (buildT T0)). apply varD_tail; trivial. apply varD_tail_rev; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)