kijeong-lim / dschingiskhan Goto Github PK

Lemma in_build_iff (psi : AczelSet -> AczelSet -> Prop) :
  forall X : AczelSet,
  forall Y : AczelSet,
  elem Y (build psi X) <-> (exists x : AczelSet, elem x X /\ psi x Y).

Lemma strong_collection (psi : AczelSet -> AczelSet -> Prop) :
  forall X : AczelSet,
  (forall x : AczelSet, elem x X -> exists y : AczelSet, psi x y) ->
  (forall x : AczelSet, elem x X -> exists y : AczelSet, elem y (build psi X) /\ psi x y) /\ (forall y : AczelSet, elem y (build psi X) -> exists x : AczelSet, elem x X /\ psi x y).
Proof with eauto with *.
  intros X H.
  split.
  - intros x H0.
    destruct (H x H0) as [y H1].
    assert (H2 : exists x : AczelSet, elem x X /\ psi x y) by firstorder.
    assert (H3 := proj2 (in_build_iff psi X y) H2)...
  - intros y H0.
    apply in_build_iff...
Qed.