proposition: Lemma terms_conv_var_usage : forall M N Q x y, (forall A B, activeEnv M |= x := A -> activeEnv N |= y := B -> A = B) -> envSub Q x y -> conv_term (term M) (term N) Q -> activeEnv_compSubst_on M N x y.
proof: Proof. destruct M as [E Pt T M]; induction M; intros; inversion H1. intro A0; unfold VarD. term_inv N; split; intro D. destruct (@activeEnv_var_det (buildT (TVar v)) x x0 A0); trivial. assert (x2 = y). inversion H3; rewrite <- H9. apply (envSub_Lok Q x y0 y); trivial. rewrite <- H6; trivial. assert (A0 = A1). rewrite H7; simpl. apply H. simpl in H7. rewrite <- H7; rewrite <- H7 in D; trivial. change (copy x2 None ++ A1 [#] EmptyEnv) with (activeEnv (buildT (TVar T))). apply activeEnv_var_decl; trivial. rewrite <- H8; trivial. rewrite <- H8; trivial. rewrite H8; rewrite H9. unfold decl, EmptyEnv; apply nth_after_copy. destruct (@activeEnv_var_det (buildT (TVar T)) x2 y A0); trivial. assert (x = x0). apply (envSub_Rok Q x x0 y); trivial. inversion H3. rewrite H6; rewrite <- H9; trivial. assert (A = A0). rewrite H7; simpl. apply H. change (copy x None ++ A [#] EmptyEnv) with (activeEnv (buildT (TVar v))). apply activeEnv_var_decl; trivial. rewrite <- H8; trivial. rewrite <- H8; trivial. simpl in H7. rewrite <- H7; rewrite <- H7 in D; trivial. rewrite H8; rewrite H9. unfold decl, EmptyEnv; apply nth_after_copy. term_inv N; split; destruct x; destruct y; try_solve. intro A1; clear S H3. term_inv N. assert (Qii: envSub (envSubst_lift1 Q) (S x) (S y)). destruct Q; trivial. assert (Conv: conv_term Pt (term (buildT T)) (envSubst_lift1 Q)). simpl; inversion H5; rewrite <- H8; trivial. assert (Econv: forall A B, activeEnv (buildT M) |= S x := A -> activeEnv (buildT T) |= S y := B -> A = B). intros; apply H. apply varD_tail; trivial. apply varD_tail; trivial. set (hint := IHM (buildT T) (envSubst_lift1 Q) (S x) (S y) Econv Qii Conv A1). fold (activeEnv (buildT M)) in *; fold (activeEnv (buildT T)). split; intro D. apply varD_tail. apply (proj1 hint). apply varD_tail_rev; trivial. apply varD_tail. apply (proj2 hint). apply varD_tail_rev; trivial. term_inv N; intro A1; simpl. fold (activeEnv (buildT M1)) in *; fold (activeEnv (buildT T1)) in * . fold (activeEnv (buildT M2)) in *; fold (activeEnv (buildT T2)) in * . inversion H4. rewrite H9 in H5. rewrite H10 in H7. assert (EcompL: forall A B, activeEnv (buildT M1) |= x := A -> activeEnv (buildT T1) |= y := B -> A = B). intros C D LC RD. apply H. apply env_sum_ly; trivial. apply (activeEnv_app_comp (buildT (TApp M1 M2)) I); trivial. apply env_sum_ly; trivial. apply (activeEnv_app_comp (buildT (TApp T1 T2)) I); trivial. assert (EcompR: forall A B, activeEnv (buildT M2) |= x := A -> activeEnv (buildT T2) |= y := B -> A = B). intros C D LC RD. apply H. apply env_sum_ry; trivial. apply env_sum_ry; trivial. split; intro D. destruct (env_sum_varDecl (activeEnv (buildT M1)) (activeEnv (buildT M2)) D) as [[l _] | r]. apply env_sum_ly. exact (@activeEnv_app_comp (buildT (TApp T1 T2)) I y). apply (proj1 (IHM1 (buildT T1) Q x y EcompL H0 H5 A1)); trivial. apply env_sum_ry. apply (proj1 (IHM2 (buildT T2) Q x y EcompR H0 H7 A1)); trivial. destruct (env_sum_varDecl (activeEnv (buildT T1)) (activeEnv (buildT T2)) D) as [[l _] | r]. apply env_sum_ly. exact (@activeEnv_app_comp (buildT (TApp M1 M2)) I x). apply (proj2 (IHM1 (buildT T1) Q x y EcompL H0 H5 A1)); trivial. apply env_sum_ry. apply (proj2 (IHM2 (buildT T2) Q x y EcompR H0 H7 A1)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)