proposition: Lemma fundamental {Γ s P} : typing Γ P s -> forall σ τ ρ, C (fun n => match List.nth_error Γ n with Some x => x | _ => poly_abs (poly_var 0) end) ρ τ -> E s ρ (subst_term σ τ P).
proof: Proof. induction 1 as [Γ n s H | | Γ | | ]; intros σ τ ρ HC. - specialize (HC n). cbn in HC. rewrite H in HC. eapply HC. - cbn. eapply E_app; eauto. - eapply E_lam; fold subst_term. + eapply R_sn. eapply IHtyping. eapply C_ext. 4:{ eapply C_up, HC. } all: try reflexivity. now intros []. + intros ξ1 ξ2 Q HQ. match goal with [ |- E _ _ ?R] => replace R with (subst_term (σ >> ren_poly_type ξ1) (Q .: τ >> ren_term ξ1 ξ2) P) end. * eapply IHtyping. eapply C_ext. 4:{ eapply C_scons. eauto. eapply C_rename, HC. } all: try reflexivity. intros []; cbn; try reflexivity. * asimpl. eapply ext_term. intros. asimpl. -- erewrite rinst_inst_poly_type; reflexivity. -- intros []. reflexivity. asimpl. erewrite rinst_inst_term; try reflexivity. now asimpl. - cbn. eapply E_tapp; eauto. - cbn. eapply E_tlam. + specialize (IHtyping (up_poly_type_poly_type σ) (τ >> ren_term shift id) ((fun _ => False) .: ρ)). eapply R_sn. refine (IHtyping _). intros n. rewrite List.nth_error_map. destruct List.nth_error eqn:Eq. * cbn. asimpl. eapply E_weaken. specialize (HC n). cbn in HC. rewrite Eq in HC. eapply R_ren, HC. * unfold ssrfun.Option.map, ssrfun.Option.bind, ssrfun.Option.apply. eapply R_ren. specialize (HC n). cbn in HC. rewrite Eq in HC. eapply HC. + intros ξ p t. asimpl. eapply IHtyping. intros n. asimpl. eapply R_ext. 2:reflexivity. 2:{ eapply E_weaken. erewrite <- rinst_inst_term; try reflexivity. eapply R_ren. eapply HC. } * f_equal. rewrite List.nth_error_map. now destruct List.nth_error eqn:Eq. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms