proposition: Lemma well_founded_RA_of_opt B (f : B -> option A) (wf_A : well_founded RA) : well_founded (fun x y => match f x, f y with | Some fx, Some fy => RA fx fy | _, _ => False end).
proof: Proof. intro a. destruct (f a) eqn:H. { eapply Acc_RA_of_opt, wf_A; eassumption. } { constructor. intro y. destruct (f y); [ rewrite H | ]; intros []. } Defined.
imports: Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Coq.Lists.SetoidList Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat