Here is a proof that appears in this online course https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html#lab222.
Proof with eauto.
remember (@empty ty) as Gamma.
intros t t' T HT. generalize dependent t'.
induction HT;
intros t' HE; subst Gamma; subst;
try solve [inversion HE; subst; auto].
- (* T_App *)
inversion HE; subst...
(* Most of the cases are immediate by induction,
and [eauto] takes care of them *)
+ (* ST_AppAbs *)
apply substitution_preserves_typing with T11...
inversion HT1...
Qed.
What do the ellipses do in this line?
apply substitution_preserves_typing with T11...
Ellipses apply a certain predefined tactic. In this proof, it's eauto
since the proof started with Proof with eauto
. See the reference manual for more.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With