equal
deleted
inserted
replaced
141 by (intro has_type_subst_closed); |
141 by (intro has_type_subst_closed); |
142 with s' t mgu_ok; show ?thesis; by simp; |
142 with s' t mgu_ok; show ?thesis; by simp; |
143 qed; |
143 qed; |
144 show "$ s a |- e2 :: $ u t2"; |
144 show "$ s a |- e2 :: $ u t2"; |
145 proof -; |
145 proof -; |
146 from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; |
146 from hyp2 W2_ok [RS sym]; |
147 by blast; |
147 have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; |
148 hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; |
148 hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; |
149 by (rule has_type_subst_closed); |
149 by (rule has_type_subst_closed); |
150 with s'; show ?thesis; by simp; |
150 with s'; show ?thesis; by simp; |
151 qed; |
151 qed; |
152 qed; |
152 qed; |