proposition: Lemma is_guarded_inj_disjoint_union_aux {A B: Type} (P1 P2 P: A -> Prop) (f: A -> B) (g1 g2: B -> option A): Prop_join P1 P2 P -> is_rev_fun P1 f g1 -> is_rev_fun P2 f g2 -> (forall a1 a2, P1 a1 -> P2 a2 -> f a1 <> f a2) -> let g := fun b => match g1 b with Some a => Some a | _ => g2 b end in is_rev_fun P f g.
proof: Proof. intros. destruct H. intro b. specialize (H0 b); specialize (H1 b). subst g; cbv beta. destruct (g1 b); [| destruct (g2 b)]. + split; [firstorder |]. intros. rewrite H in H4; destruct H4. - apply (proj2 H0); auto. - pose proof proj2 (proj2 H0 a (proj1 H0)) eq_refl. split; intros. * exfalso. apply (H2 a a0 (proj1 H0) H4). congruence. * subst a; auto. + split; [firstorder |]. intros. rewrite H in H4; destruct H4. - pose proof proj2 (proj2 H1 a (proj1 H1)) eq_refl. split; intros. * exfalso. apply (H2 a0 a H4 (proj1 H1)). congruence. * subst a; auto. - apply (proj2 H1); auto. + intros. rewrite H in H4; firstorder. 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