Solution for Rules.triple_let_val
Lemma triple_let_val : forall x v1 t2 H Q,
triple (subst x v1 t2) H Q ->
triple (trm_let x v1 t2) H Q.
Proof using.
dup.
{ (* first proof *)
introv M. applys triple_let. applys triple_conseq_frame.
{ applys triple_val_minimal. } { xsimpl. } { xsimpl. }
{ simpl. intros v. applys triple_hpure. intros ->. applys M. } }
{ (* second proof *)
introv M. applys triple_let (fun v => \[v = v1] \* H).
{ applys triple_val. xsimpl. auto. }
{ intros v. applys triple_hpure. intros ->. applys M. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
