proposition: Lemma wf_opt A (R : relation A) : WF R -> WF (opt R).
proof: Proof. intros h p. destruct p. gen (h a); revert a; induction 1. apply SN_intro; intros [y|] hy; inversion hy; clear hy; subst. fo. apply SN_intro; intros [y|] hy; inversion hy. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path) CoLoR(SetUtil)