proposition: Lemma apply_variable : forall M, isArrowType M.(type) -> exists MA: Term, exists Mapp: isApp MA, (appBodyL Mapp) ~ M /\ term (appBodyR Mapp) = %length (env M) /\ env MA = env M ++ Some (type_left (type M))::EmptyEnv.
proof: Proof. intros M MA. destruct M as [ME MPt [T | A B] M]; try_solve. set (newVarEnv := copy (length ME) None ++ (Some A::EmptyEnv)). assert (RL: newVarEnv [+] ME |- MPt := A --> B). apply typing_ext_env_l; trivial. assert (RR: newVarEnv [+] ME |- %(length ME) := A). constructor. apply env_sum_ly_rn. unfold newVarEnv, VarD. rewrite nth_app_right; autorewrite with datatypes using auto. rewrite Nat.sub_diag; trivial. left; apply nth_beyond; auto. assert (envOk: env (buildT RL) = env (buildT RR)); trivial. assert (Larr: isArrowType (type (buildT RL))); trivial. assert (TypOk: type_left (type (buildT RL)) = type (buildT RR)); trivial. set (w := Build_appCond (buildT RL) (buildT RR) envOk Larr TypOk). exists (buildApp w). exists (buildApp_isApp w); repeat split; simpl. apply terms_conv_criterion. simpl; apply env_comp_ext_l. trivial. unfold newVarEnv. rewrite env_sum_disjoint; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)