Dear friends,

I solved exercise, but I feel like my definition is not what was expected by authors.

It is a very last exercise in this chapter.

https://softwarefoundations.cis.upenn.edu/current/plf-current/Equiv.html

#### Exercise: 4 stars, advanced, optional (capprox)

Second task:

```
(* Find a program cmin that approximates every other program.
Definition capprox (c1 c2 : com) : Prop := forall (st st' : state),
st =[ c1 ]-> st' -> st =[ c2 ]-> st'.
Theorem skip_left : forall c,
cequiv
(SKIP;; c)
c.
*)
Definition cmin c : com := SKIP ;; c.
Theorem cmin_minimal : forall c, capprox (cmin c) c.
Proof. unfold capprox.
unfold cmin.
intros.
induction c; apply skip_left; apply H.
Qed.
```

If feel like my definition of cmin is meaninglessâ€¦ please advice

Thank you very much.