proposition: Lemma apply_var_comp : forall M A B, Computable M -> type M = A --> B -> (forall P, type P = A -> algebraic P -> isNeutral P -> (forall S, P -R-> S -> Computable S) -> Computable P) -> exists Mx, exists Mx_app: isApp Mx, (appBodyL Mx_app) ~ M /\ term (appBodyR Mx_app) = %(length (env M)) /\ env Mx = env M ++ Some A :: EmptyEnv /\ Computable Mx.
proof: Proof. intros M C D Mcomp MT IH. destruct (apply_variable M) as [Mx [Mx_app [MxL [MxR Mx_env]]]]. rewrite MT; simpl; trivial. exists Mx; exists Mx_app; split; trivial. repeat split; trivial. rewrite MT in Mx_env; try_solve. apply comp_app with Mx_app. rewrite MxL; trivial. apply IH. apply app_typeR with D. rewrite <- terms_conv_eq_type with M (appBodyL Mx_app); trivial. term_inv Mx; destruct T2; try_solve. apply terms_conv_sym; trivial. apply algebraic_var; apply var_is_var with (length (env M)); trivial. apply var_neutral. eapply var_is_var; eauto. intros S RS. absurd (appBodyR Mx_app -R-> S); auto with comp. apply R_var_normal. apply var_is_var with (length (env M)); try_solve. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)