proposition: Lemma is_guarded_inj_disjoint_union {A B: Type} (P1 P2 P: A -> Prop) (f: A -> B): Prop_join P1 P2 P -> is_guarded_inj P1 f -> is_guarded_inj P2 f -> (forall a1 a2, P1 a1 -> P2 a2 -> f a1 <> f a2) -> is_guarded_inj P f.
proof: Proof. intros. destruct H0 as [g1 ?], H1 as [g2 ?]. exists (fun b => match g1 b with Some a => Some a | _ => g2 b end). eapply is_guarded_inj_disjoint_union_aux; eauto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext