proposition: Lemma disjunctive_wf : forall (A:Type) (T R1 R2 : A -> A -> Prop) (decR1 : dec_rel R1) (decR2 : dec_rel R2), well_founded R1 -> well_founded R2 -> (forall x y, clos_trans_1n A T x y -> R1 x y \/ R2 x y) -> well_founded T.
proof: Proof. intros A T R1 R2 decR1 decR2 wfR1 wfR2 Hincl. pose (R x y := ~ R1 y x /\ ~ R2 y x). assert (almost_full R) as Raf. apply af_intersection. apply (af_from_wf wfR1 decR1). apply (af_from_wf wfR2 decR2). apply wf_from_af with (R:=R). intros x y CT. destruct CT; firstorder. assumption. Defined.
imports: Coq(Relations) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)