Solution for Rules.ProofsSameSemantics.eta_same_triples
intros. iff M.
{ applys triple_eval_like M. applys eval_like_eta_reduction. }
{ applys triple_eval_like M. applys eval_like_eta_expansion. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback