More than 5 years have passed since last update.
assign_equiv.v
(** **** 練習問題: ★★, recommended (assign_aequiv) *)Theoremassign_aequiv:forallXe,aequiv(AIdX)e->cequivSKIP(X::=e).Proof.move=>XeH.split=>HH.-inversionHH.subst.assert(st'=updatest'X(st'X)).-applyfunctional_extensionality=>x.byrewriteupdate_same;reflexivity.-set(Hass:=E_Assst'e(st'X)X).rewrite<-H0inHass.applyHass.rewrite<-(Hst').reflexivity.-inversionHH.subst.replace(updatestX(aevalste))withst.-constructor.-applyfunctional_extensionality=>x.rewrite<-(Hst).rewriteupdate_same;reflexivity.Qed.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme