Solution for Triples.seval_seq
introv M1 M2. gen_eq Q1': Q1.
induction M1; intros; subst.
{ apply seval_step.
{ do 2 esplit. applys step_seq. }
{ introv R. inverts R as R'. { inverts R'. } applys* M2. } }
{ rename t into t1, H1 into IH.
destruct H as (s'&t'&RE). applys seval_step.
{ do 2 esplit. constructors. applys RE. }
{ introv R. inverts R as R'.
{ applys* IH R' M2. }
{ false. inverts RE. } } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
