Solution for Rules.ProofsSameSemantics.triple_trm_seq_assoc
introv M. applys triple_eval_like M. clear M.
introv R. inverts R as. introv R1 R3. inverts R1 as. introv R1 R2.
applys eval_seq R1. introv Hs2. applys eval_seq.
{ applys* R2. } { intros. applys* R3. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
