Require Import Computation.Monad.
-(* decomposition lemma *)
+(** A decomposition lemma *)
Definition decomp (A:Set)(c:#A) : #A :=
match c with
| Return x => Return x
end.
Implicit Arguments decomp.
-(* decomposition theorem: we can always decompose *)
+(** A decomposition theorem: we can always decompose *)
Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
intros A l; case l; simpl; trivial.
Qed.
-(* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
+(** 1-, 2-, 3-, 4-, and 5-ary decompositions; you should use this *)
Ltac uncomp comp :=
match goal with
| [ |- context[(comp ?X)] ] =>