(*
 * Copyright (c) 2009-2011, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.sepalg.
Require Import VST.msl.psepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.cjoins.
Require Import VST.msl.eq_dec.

(** The cross split axiom looks unwieldly,
    but here we show that it arises naturally
    as a kind of distributivity property.
    Cross split can be rendered, with some accuracy,
    as "the separation algebra is distributive."
 *)

  (** This definition mirrors the definition of
      distributivity in a join-semilattice.  This
      definition generalizes the standard notion of
      distributivity in a lattice, but only mentions
      of the lattice operators.  Here we transplant
      the semilattice definition into the setting
      of separation algebras.
    *)
  Definition sa_distributive (A: Type) {JOIN: Join A} :=
    forall a b x z,
      join a b z ->
      constructive_join_sub x z ->
      {a' : A & {b' : A &
           (constructive_join_sub a' a * constructive_join_sub b' b * join a' b' x)%type}}.

(*
  (** We define this weaker version of cross-split
      in order to show that the sa_distributive
      axiom is equivalent. The ordinary cross_split
      is more constructive (it uses a sigma type rather
      than 'exists'), so we have to weaken it to show
      the correspondence.  We could, instead, define
      and use a constructive version of join_sub.
    *)
  Definition weak_cross_split `{sepalg A} :=
    forall a b c d z : A,
      join a b z ->
      join c d z ->
      exists x:(A*A*A*A), match x with (ac,ad,bc,bd) =>
         join ac ad a /\
         join bc bd b /\
         join ac bc c /\
         join ad bd d
       end.
*)

  (** Here we show that the cross split axiom is
      the same as the statement of distributivity
      for join semilattices transliterated into the
      setting of separation algebras.
    *)
  Theorem cross_split_distibutive {A} `{Perm_alg A}{SA: Sep_alg A}{CS: Cross_alg A} :
          sa_distributive A.
  Proof.
(* Goal: @sa_distributive A J *)
    intros ? ? ? ? H1 [x0 H2].
(* Goal: @sigT A (fun a' : A => @sigT A (fun b' : A => prod (prod (@constructive_join_sub A J a' a) (@constructive_join_sub A J b' b)) (@join A J a' b' x))) *)
    destruct (CS _ _ _ _ _ H1 H2) as [[[[? ?] ?] ?] ?].
(* Goal: prod (prod (@constructive_join_sub A J a0 a) (@constructive_join_sub A J a2 b)) (@join A J a0 a2 x) *)
    intuition eauto.
(* Goal: @sigT A (fun a' : A => @sigT A (fun b' : A => prod (prod (@constructive_join_sub A J a' a) (@constructive_join_sub A J b' b)) (@join A J a' b' x))) *)
    exists a0.
(* Goal: @sigT A (fun b' : A => prod (prod (@constructive_join_sub A J a0 a) (@constructive_join_sub A J b' b)) (@join A J a0 b' x)) *)
    exists a2.
(* Goal: prod (prod (@constructive_join_sub A J a0 a) (@constructive_join_sub A J a2 b)) (@join A J a0 a2 x) *)
    intuition eauto.
(* Goal: @constructive_join_sub A J a2 b *)
    econstructor; eauto.
(* Goal: @constructive_join_sub A J a2 b *)
    econstructor; eauto.
  Qed.

  Theorem distributive_cross_split {A} `{Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}:
     sa_distributive A -> Cross_alg A.
  Proof.
(* Goal: forall _ : @sa_distributive A J, @Cross_alg A J *)
    intros H0.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
    repeat intro.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    hnf in H0.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    destruct (H0 a b c z H1) as [a' [b' [[?H ?H] ?H]]].
(* Goal: @constructive_join_sub A J c z *)
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    exists d; auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    destruct H3 as [q ?H].
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    destruct H4 as [w ?H].
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A J ac ad a) (and (@join A J bc bd b) (and (@join A J ac bc c) (@join A J ad bd d)))) *)
    exists (a',q,b',w). split; auto. split; auto. split; auto.
(* Goal: @join A J q w d *)
    destruct (join_assoc H3 H1) as [f [? ?]].
(* Goal: @join A J q w d *)
    apply join_comm in H6.
(* Goal: @join A J q w d *)
    destruct (join_assoc H4 H6) as [g [? ?]].
(* Goal: @join A J q w d *)
    assert (H10: g = d); [ | rewrite H10 in *; auto].
(* Goal: @eq A g d *)
    apply join_comm in H7.
(* Goal: @eq A g d *)
    apply join_comm in H9.
(* Goal: @eq A g d *)
    destruct (join_assoc H9 H7) as [h [? ?]].
(* Goal: @eq A g d *)
    generalize (join_eq H5 (join_comm H10)); intro.
(* Goal: @eq A g d *)
    rewrite <- H12 in *; clear H12 h.
(* Goal: @eq A g d *)
    eapply join_canc; eauto.
  Qed.

(** NOTICE ABOUT REDUNDANT LEMMAS:
 Since sa_distribute <-> cross_split, many of the proofs below are redundant.
 This was part of an experiment to see whether, in general, sa_distributive is
 simpler to prove than cross_split.  Short answer:  not really.
*)

Lemma distributive_equiv: forall A, @sa_distributive  _ (@Join_equiv A).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
  repeat intro.
(* Goal: @sigT A (fun a' : A => @sigT A (fun b' : A => prod (prod (@constructive_join_sub A (Join_equiv A) a' a) (@constructive_join_sub A (Join_equiv A) b' b)) (@join A (Join_equiv A) a' b' x))) *)
 destruct H; subst.
(* Goal: @join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2) *)
 exists x; exists x; repeat split; auto.
Qed.

Lemma cross_split_equiv : forall A,  @Cross_alg _ (@Join_equiv A).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
  repeat intro.
(* Goal: @join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2) *)
  destruct H; destruct H0. subst. exists (((z,z),z),z). repeat split; auto.
Qed.

Lemma distributive_fun: forall A (JOIN: Join A) (key: Type),
               sa_distributive A -> @sa_distributive (key -> A) (Join_fun key A JOIN).
Proof.
(* Goal: forall (A : Type) (JOIN : Join A) (key : Type) (_ : @sa_distributive A JOIN), @sa_distributive (forall _ : key, A) (Join_fun key A JOIN) *)
unfold sa_distributive; intros.
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
assert (forall k, constructive_join_sub (x k) (z k)).
(* Goal: forall k : key, @constructive_join_sub A JOIN (x k) (z k) *)
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
destruct X0 as [y ?].
(* Goal: forall k : key, @constructive_join_sub A JOIN (x k) (z k) *)
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
intro k; exists (y k); auto.
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
assert (J := fun (k: key) => X (a k) (b k) (x k) (z k) (H k) (X1 k)).
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
clear X.
(* Goal: @sigT (forall _ : key, A) (fun a' : forall _ : key, A => @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) a' a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) a' b' x))) *)
exists (fun k => projT1 (J k)).
(* Goal: @sigT (forall _ : key, A) (fun b' : forall _ : key, A => prod (prod (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) (fun k : key => @projT1 A (fun a' : A => @sigT A (fun b'0 : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b'0 (b k))) (@join A JOIN a' b'0 (x k)))) (J k)) a) (@constructive_join_sub (forall _ : key, A) (Join_fun key A JOIN) b' b)) (@join (forall _ : key, A) (Join_fun key A JOIN) (fun k : key => @projT1 A (fun a' : A => @sigT A (fun b'0 : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b'0 (b k))) (@join A JOIN a' b'0 (x k)))) (J k)) b' x)) *)
exists (fun k => projT1 (projT2 (J k))).
(* Goal: prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B b1' b2') (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2)) *)
split; [split|].
exists (fun k => proj1_sig (fst (fst (projT2 (projT2 (J k))))));
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
intro k; destruct (J k) as [ak' [bk' [[c c0] j]]];  simpl; destruct c; auto.
exists (fun k => proj1_sig (snd (fst (projT2 (projT2 (J k))))));
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
intro k; destruct (J k) as [ak' [bk' [[c c0] j]]];  simpl; destruct c0; auto.
(* Goal: @join (forall _ : key, A) (Join_fun key A JOIN) (fun k : key => @projT1 A (fun a' : A => @sigT A (fun b' : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b' (b k))) (@join A JOIN a' b' (x k)))) (J k)) (fun k : key => @projT1 A (fun b' : A => prod (prod (@constructive_join_sub A JOIN (@projT1 A (fun a' : A => @sigT A (fun b'0 : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b'0 (b k))) (@join A JOIN a' b'0 (x k)))) (J k)) (a k)) (@constructive_join_sub A JOIN b' (b k))) (@join A JOIN (@projT1 A (fun a' : A => @sigT A (fun b'0 : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b'0 (b k))) (@join A JOIN a' b'0 (x k)))) (J k)) b' (x k))) (@projT2 A (fun a' : A => @sigT A (fun b' : A => prod (prod (@constructive_join_sub A JOIN a' (a k)) (@constructive_join_sub A JOIN b' (b k))) (@join A JOIN a' b' (x k)))) (J k))) x *)
intro k; destruct (J k) as [ak' [bk' [[c c0] j]]]; simpl; auto.
Qed.

Instance cross_split_fun: forall A (JOIN: Join A) (key: Type),
          Cross_alg A -> Cross_alg (key -> A).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
repeat intro.
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (f (x: key) := projT1 (X (a x) (b x) (c x) (d x) (z x) (H x) (H0 x))).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (g (x: key) := projT2 (X (a x) (b x) (c x) (d x) (z x) (H x) (H0 x))).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (ac (x: key) := fst (fst (fst (f x)))).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (ad (x: key) := snd (fst (fst (f x)))).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (bc (x: key) := snd (fst (f x))).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
pose (bd (x: key) := snd (f x)).
(* Goal: @sigT (prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A)) (fun x : prod (prod (prod (forall _ : key, A) (forall _ : key, A)) (forall _ : key, A)) (forall _ : key, A) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d)))) *)
exists (ac,ad,bc,bd).
(* Goal: and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac ad a) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) bc bd b) (and (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ac bc c) (@join (forall _ : key, A) (Join_pi key (fun _ : key => A) (fun _ : key => JOIN)) ad bd d))) *)
unfold ac, ad, bc, bd, f; clear ac ad bc bd f.
repeat split; intro x; simpl;
(* Goal: and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) d Hd)))) *)
generalize (g x);  destruct (projT1 (X (a x) (b x) (c x) (d x) (z x) (H x) (H0 x))) as [[[? ?] ?] ?]; simpl; intuition.
Qed.

Lemma sa_distributive_prod : forall A B saA saB,
  @sa_distributive A saA ->
  @sa_distributive B saB ->
  @sa_distributive (A * B) (Join_prod A _ B _).
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
 intros.
(* Goal: @sa_distributive (prod A B) (Join_prod A saA B saB) *)
 intros [a1 a2] [b1 b2] [c1 c2] [z1 z2] [? ?].
(* Goal: forall _ : @constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B c1 c2) (@pair A B z1 z2), @sigT (prod A B) (fun a' : prod A B => @sigT (prod A B) (fun b' : prod A B => prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) a' (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) b' (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) a' b' (@pair A B c1 c2)))) *)
 intros [[d1 d2] [? ?]].
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
 simpl in *.
(* Goal: @sigT (prod A B) (fun a' : prod A B => @sigT (prod A B) (fun b' : prod A B => prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) a' (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) b' (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) a' b' (@pair A B c1 c2)))) *)
 destruct (X a1 b1 c1 z1 H) as [a1' [b1' [[[u1 ?] [v1 ?]] ?]]]. exists d1; auto.
(* Goal: @sigT (prod A B) (fun a' : prod A B => @sigT (prod A B) (fun b' : prod A B => prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) a' (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) b' (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) a' b' (@pair A B c1 c2)))) *)
 destruct (X0 a2 b2 c2 z2 H0) as [a2' [b2' [[[u2 ?] [v2 ?]] ?]]]. exists d2; auto.
(* Goal: @sigT (prod A B) (fun a' : prod A B => @sigT (prod A B) (fun b' : prod A B => prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) a' (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) b' (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) a' b' (@pair A B c1 c2)))) *)
 exists (a1',a2'). exists (b1',b2').
(* Goal: prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B b1' b2') (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2)) *)
 split; [split|].
(* Goal: @join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2) *)
 exists (u1,u2); split; auto.
(* Goal: @join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2) *)
 exists (v1,v2); split; auto.
(* Goal: @join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2) *)
 split; auto.
Qed.

Instance Cross_prod : forall A B saA saB,
  @Cross_alg A saA ->
  @Cross_alg B saB ->
  @Cross_alg (A * B) (Join_prod _ saA _ saB).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
  repeat intro.
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad a) (and (@join (prod A B) (Join_prod A saA B saB) bc bd b) (and (@join (prod A B) (Join_prod A saA B saB) ac bc c) (@join (prod A B) (Join_prod A saA B saB) ad bd d)))) *)
  destruct a as [a1 a2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd b) (and (@join (prod A B) (Join_prod A saA B saB) ac bc c) (@join (prod A B) (Join_prod A saA B saB) ad bd d)))) *)
  destruct b as [b1 b2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc c) (@join (prod A B) (Join_prod A saA B saB) ad bd d)))) *)
  destruct c as [c1 c2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd d)))) *)
  destruct d as [d1 d2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  destruct z as [z1 z2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  destruct H.
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  destruct H0.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  simpl in *.
  destruct (X a1 b1 c1 d1 z1)
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
    as [p ?]; auto.
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  destruct p as [[[s1 p1] q1] r1].
  destruct (X0 a2 b2 c2 d2 z2)
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
    as [p ?]; auto.
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  destruct p as [[[s2 p2] q2] r2].
(* Goal: @sigT (prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B)) (fun x : prod (prod (prod (prod A B) (prod A B)) (prod A B)) (prod A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (prod A B) (Join_prod A saA B saB) ac ad (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) bc bd (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) ac bc (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) ad bd (@pair A B d1 d2))))) *)
  exists ((s1,s2),(p1,p2),(q1,q2),(r1,r2)).
(* Goal: and (@join (prod A B) (Join_prod A saA B saB) (@pair A B s1 s2) (@pair A B p1 p2) (@pair A B a1 a2)) (and (@join (prod A B) (Join_prod A saA B saB) (@pair A B q1 q2) (@pair A B r1 r2) (@pair A B b1 b2)) (and (@join (prod A B) (Join_prod A saA B saB) (@pair A B s1 s2) (@pair A B q1 q2) (@pair A B c1 c2)) (@join (prod A B) (Join_prod A saA B saB) (@pair A B p1 p2) (@pair A B r1 r2) (@pair A B d1 d2)))) *)
  simpl; intuition; (split; simpl; auto).
Qed.

Lemma sa_distributive_bij : forall A B JA bij,
  @sa_distributive A JA ->
  @sa_distributive B (Join_bij A JA B bij).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
 repeat intro.
(* Goal: @sigT B (fun a' : B => @sigT B (fun b' : B => prod (prod (@constructive_join_sub B (Join_bij A JA B bij) a' a) (@constructive_join_sub B (Join_bij A JA B bij) b' b)) (@join B (Join_bij A JA B bij) a' b' x))) *)
 destruct X0 as [u ?]. unfold Join_bij; simpl.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
 destruct bij. simpl.
(* Goal: @sigT B (fun a' : B => @sigT B (fun b' : B => prod (prod (@constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) a' a) (@constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) b' b)) (@join B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) a' b' x))) *)
 destruct (X (bij_g a) (bij_g b) (bij_g x) (bij_g z)) as [a' [b' [[[? ?] [? ?]] ?]]]; auto.
(* Goal: @constructive_join_sub A JA (bij_g x) (bij_g z) *)
(* Goal: @sigT B (fun a' : B => @sigT B (fun b' : B => prod (prod (@constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) a' a) (@constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) b' b)) (@join B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) a' b' x))) *)
 exists (bij_g u); auto.
(* Goal: prod (prod (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B a1 a2)) (@constructive_join_sub (prod A B) (Join_prod A saA B saB) (@pair A B b1' b2') (@pair A B b1 b2))) (@join (prod A B) (Join_prod A saA B saB) (@pair A B a1' a2') (@pair A B b1' b2') (@pair A B c1 c2)) *)
 exists (bij_f a'); exists (bij_f b'); split; [split|].
(* Goal: @constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f a') a *)
(* Goal: @constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f b') b *)
(* Goal: @join B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f a') (bij_f b') x *)
 exists (bij_f x0); hnf; repeat rewrite bij_gf; auto.
(* Goal: @constructive_join_sub B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f b') b *)
(* Goal: @join B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f a') (bij_f b') x *)
 exists (bij_f x1); hnf; repeat rewrite bij_gf; auto.
(* Goal: @join B (fun x y z : B => @join A JA (bij_g x) (bij_g y) (bij_g z)) (bij_f a') (bij_f b') x *)
 hnf; repeat rewrite bij_gf; auto.
Qed.

Lemma Cross_bij : forall A B JA bij,
  @Cross_alg A  JA ->
  @Cross_alg B (Join_bij A JA B bij).
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
  repeat intro. unfold join, Join_bij in *.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct bij. simpl in *.
(* Goal: @sigT (prod (prod (prod B B) B) B) (fun x : prod (prod (prod B B) B) B => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA (bij_g ac) (bij_g ad) (bij_g a)) (and (@join A JA (bij_g bc) (bij_g bd) (bij_g b)) (and (@join A JA (bij_g ac) (bij_g bc) (bij_g c)) (@join A JA (bij_g ad) (bij_g bd) (bij_g d))))) *)
  destruct (X (bij_g a) (bij_g b) (bij_g c) (bij_g d) (bij_g z)); auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct x as [[[s p] q] r].
(* Goal: @sigT (prod (prod (prod B B) B) B) (fun x : prod (prod (prod B B) B) B => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA (bij_g ac) (bij_g ad) (bij_g a)) (and (@join A JA (bij_g bc) (bij_g bd) (bij_g b)) (and (@join A JA (bij_g ac) (bij_g bc) (bij_g c)) (@join A JA (bij_g ad) (bij_g bd) (bij_g d))))) *)
  exists (bij_f s,bij_f p,bij_f q,bij_f r).
(* Goal: and (@join A JA (bij_g (bij_f s)) (bij_g (bij_f p)) (bij_g a)) (and (@join A JA (bij_g (bij_f q)) (bij_g (bij_f r)) (bij_g b)) (and (@join A JA (bij_g (bij_f s)) (bij_g (bij_f q)) (bij_g c)) (@join A JA (bij_g (bij_f p)) (bij_g (bij_f r)) (bij_g d)))) *)
  simpl.
(* Goal: and (@join A JA (bij_g (bij_f s)) (bij_g (bij_f p)) (bij_g a)) (and (@join A JA (bij_g (bij_f q)) (bij_g (bij_f r)) (bij_g b)) (and (@join A JA (bij_g (bij_f s)) (bij_g (bij_f q)) (bij_g c)) (@join A JA (bij_g (bij_f p)) (bij_g (bij_f r)) (bij_g d)))) *)
  repeat rewrite bij_gf.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  auto.
Qed.

Lemma constructive_join_sub_smash {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A}:
  (forall x:A, {identity x}+{~identity x}) ->
  forall a c : lifted JA,
    constructive_join_sub (proj1_sig a) (proj1_sig c) ->
    @constructive_join_sub (option (lifted JA)) _ (Some a) (Some c).
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
intros.
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
destruct X0 as [b ?].
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
destruct (X b).
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
assert (a=c).
(* Goal: @eq (@lifted A JA) a c *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
destruct a; destruct c. apply exist_ext.
(* Goal: @eq A x x0 *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
simpl in j.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
eapply join_eq; try apply j. apply join_comm; apply identity_unit; eauto.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
subst c.
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) a) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
exists None; constructor.
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
exists (Some (mk_lifted _ (nonidentity_nonunit n))).
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
constructor.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
destruct a; destruct c; simpl in *.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
auto.
Qed.

Lemma sa_distributive_smash : forall A JA {PA: Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A},
  (forall x:A, {identity x}+{~identity x}) ->
  @sa_distributive A JA ->
  sa_distributive (option (lifted JA)).
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
intros. unfold Join_lower, Join_lift; simpl.
intros [[a Ha]|].
2: intros; assert (b=z) by (inv H; auto); subst z; exists None; exists x;
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    split; [split|]; auto; [ econstructor  | ]; constructor.
intros [[b Hb]|].
2: intros b [[z Hz]|] ? ?;
 [assert (a=z) by (inv H; auto); subst z; clear H;
   rewrite (proof_irr Hz Ha) in X1; clear Hz; exists b; exists None;
    split; [split|]; auto
 | elimtype False; inv H];
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
  [ econstructor  | ]; constructor.
intros [[c Hc]|].
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
2: intros ? ? ?; exists None; exists None; split; [split|]; econstructor; econstructor.
intros [[z Hz]|] H Hj.
2: elimtype False; inv H.
destruct (X0 a b c z) as [a' [b' [[? ?] ?]]].
inv H. apply H3.
inversion Hj.
destruct x.
exists (lifted_obj l). inv H0.  apply H4.
assert (c=z) by (inv H0; auto). replace c with z.
apply constructive_join_sub_refl.
destruct (X a') as [Pa'|Pa']; [exists None | exists (Some (mk_lifted _ (nonidentity_nonunit Pa'))) ].
assert (b'=c) by (eapply join_eq; try apply j; apply identity_unit; eauto).
subst b'.
exists (Some (mk_lifted c Hc)).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
split; [split|]; eauto. econstructor; econstructor.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
apply constructive_join_sub_smash; auto.
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
constructor.
destruct (X b') as [Pb'|Pb']; [exists None | exists (Some (mk_lifted _ (nonidentity_nonunit Pb')))].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
split; [split|]; eauto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
apply constructive_join_sub_smash; auto.
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
econstructor; econstructor.
(* Goal: @constructive_join_sub A J a2 b *)
apply join_unit2. econstructor; eauto.
(* Goal: @eq (@lifted A JA) (@exist A (@nonunit A JA) x n) (@exist A (@nonunit A JA) x0 n0) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
(* Goal: @constructive_join_sub (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) c) *)
f_equal. apply exist_ext.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
symmetry. eapply join_eq. eapply join_comm; apply j.  apply identity_unit; eauto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
split; [split|]; eauto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
apply constructive_join_sub_smash; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
apply constructive_join_sub_smash; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
constructor; auto.
Qed.

Lemma Cross_smash : forall A (JA: Join A) {PA: Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A},
  (forall x:A, {identity x}+{~identity x}) ->
  Cross_alg A ->
  Cross_alg (option (lifted JA)).
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  hnf; intros.
  destruct a as [[a Na] | ].
2:{
  apply join_unit1_e in H; [ | apply None_identity]. subst z.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None,None,c,d); repeat split; auto; constructor; auto.
}
  destruct b as [[b Nb] | ].
2:{
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  apply join_unit2_e in H; [ | apply None_identity]. subst z.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (c,d,None,None); repeat split; auto; constructor; auto.
}
  destruct c as [[c Nc] | ].
2:{
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  apply join_unit1_e in H0; [ | apply None_identity]. subst z.
  exists (None, Some (exist nonunit _ Na), None, Some (exist nonunit _ Nb));
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
     repeat split; auto; constructor.
}
  destruct d as [[d Nd] | ].
2:{
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  apply join_unit2_e in H0; [ | apply None_identity]. subst z.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (Some (exist nonunit _ Na), None,Some (exist nonunit _ Nb),None); repeat split; auto; constructor; auto.
}
  destruct z as [[z Nz] | ]; [ | elimtype False; inv H].
  destruct (X0 a b c d z) as [[[[ac ad] bc] bd] [? [? [? ?]]]]; try (inv H; inv H0; auto). clear H H0.
  destruct (X ac) as [Nac | Nac ].
  apply Nac in H1. subst ad. apply Nac in H3. subst bc.
  destruct (X bd) as [Nbd | Nbd].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H4; auto. subst d.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H2; auto. subst c.
  rewrite (proof_irr Nd Na) in *. rewrite (proof_irr Nc Nb) in *.
  exists (None, Some (exist nonunit a Na), Some (exist nonunit b Nb), None);
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    repeat split; auto;  constructor.
  exists (None, Some (exist nonunit a Na), Some (exist nonunit c Nc),
      Some (exist nonunit bd (nonidentity_nonunit Nbd))).
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
  repeat split; auto;  try constructor. apply H2. apply H4.
  destruct (X ad) as [Nad | Nad].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H1; auto. subst ac.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit1_e in H4; auto. subst bd.
  destruct (X bc) as [Nbc | Nbc].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H3; auto. subst c.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit1_e in H2; auto. subst d.
  rewrite (proof_irr Nd Nb) in *. rewrite (proof_irr Nc Na) in *.
  exists (Some (exist nonunit a Na), None, None, Some (exist nonunit b Nb));
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    repeat split; auto; constructor.
  apply nonidentity_nonunit in Nbc.
  exists (Some (exist nonunit a Na), None, Some (exist nonunit _ Nbc), Some (exist nonunit d Nd));
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    repeat split; auto; constructor. apply H2. apply H3.
  destruct (X bc) as [Nbc | Nbc].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H3; auto. subst ac.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit1_e in H2; auto. subst bd.
  apply nonidentity_nonunit in Nad.
  exists (Some (exist nonunit c Nc), Some (exist nonunit _ Nad), None, Some (exist nonunit b Nb));
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    repeat split; auto; try constructor. apply H1. apply H4.
  destruct (X bd) as [Nbd | Nbd].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H2; auto. subst bc.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply join_unit2_e in H4; auto. subst ad.
  apply nonidentity_nonunit in Nbc.   apply nonidentity_nonunit in Nad.
    apply nonidentity_nonunit in Nac.
  exists (Some (exist nonunit ac Nac), Some (exist nonunit d Nd),
             Some (exist nonunit b Nb), None).
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
    repeat split; auto; try constructor. apply H1. apply H3.
  apply nonidentity_nonunit in Nbc.   apply nonidentity_nonunit in Nad.
    apply nonidentity_nonunit in Nac. apply nonidentity_nonunit in Nbd.
  exists (Some (exist nonunit ac Nac), Some (exist nonunit ad Nad),
             Some (exist nonunit bc Nbc), Some (exist nonunit bd Nbd)).
  repeat split; constructor; assumption.
Qed.

Lemma cross_split_fpm : forall A B
      (JB: Join B) (PB: Perm_alg B)(SB : Sep_alg B)(CB: Disj_alg B)
  (Bdec: forall x:B, {identity x}+{~identity x}) ,
  Cross_alg B  ->
  Cross_alg (fpm A (lifted JB)) .
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @Cross_alg (fpm A (@lifted B JB)) (Join_prop (forall _ : A, option (@lifted B JB)) (Join_pi A (fun _ : A => option (@lifted B JB)) (fun _ : A => @Join_lower (@lifted B JB) (@Join_lift B JB))) (@finMap A (@lifted B JB))) *)
  assert (Cross_alg (A -> option (lifted JB))).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  apply cross_split_fun. apply Cross_smash; auto.

(* Goal: @Cross_alg (fpm A (@lifted B JB)) (Join_prop (forall _ : A, option (@lifted B JB)) (Join_pi A (fun _ : A => option (@lifted B JB)) (fun _ : A => @Join_lower (@lifted B JB) (@Join_lift B JB))) (@finMap A (@lifted B JB))) *)
  hnf. intros [a Ha] [b Hb] [c Hc] [d Hd] [z Hz].
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  simpl; intros.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  destruct (X0 a b c d z); auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct x as [[[s p] q] r].
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  decompose [and] y; clear y.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hs : finMap s).
(* Goal: @finMap A B s *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Ha.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option B) (s a0) (@None B) *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  specialize ( H1 a0).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H1; auto. inv H1; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hq : finMap q).
(* Goal: @finMap A B r *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hb.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  specialize ( H3 a0). inv H3; auto. rewrite H9; rewrite e; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H8; auto. inv H8.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hr : finMap r).
(* Goal: @finMap A B r *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hb.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option B) (r a0) (@None B) *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  specialize ( H3 a0).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H3; auto. inv H3; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hp : finMap p).
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hd.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  exists x. intros. specialize ( H5 a0). rewrite e in H5; auto. inv H5; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists (exist _ s Hs, exist _ p Hp, exist _ q Hq, exist _ r Hr).
(* Goal: and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) d Hd)))) *)
  simpl; intuition.
Qed.

Lemma Cross_fpm (A B: Type){JB: Join B} {PB: Perm_alg B}{PosB : Pos_alg B}
  {CrB: Cross_alg B}:   Cross_alg (fpm A B) .
 (* Warning: This lemma is valid, but it's not clear that it's useful *)
Proof.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (Cross_alg (A -> option B)).
(* Goal: @Cross_alg (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  apply cross_split_fun.
(* Goal: @Cross_alg (option B) (@Join_lower B JB) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  unfold Cross_alg.
(* Goal: forall (a b c d z : option B) (_ : @join (option B) (@Join_lower B JB) a b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad a) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct a as [a |]. destruct b as [b|]. destruct c as [c|]. destruct d as [d|].
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct z as [z|].
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) (@None B)) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) (@None B)), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  hnf in H.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) (@None B)) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) (@None B)), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (join a b z) by (clear - H; inv H; auto).
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) (@None B)) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) (@None B)), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (join c d z) by (clear - H0; inv H0; auto).
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) (@None B)) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) (@None B)), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  clear H H0.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) (@None B)) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@Some B d) (@None B)), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct (CrB _ _ _ _ _ H1 H2) as [[[[s p] q] r] [? [? [? ?]]]].
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (Some s, Some p, Some q, Some r); repeat split; try constructor; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros. elimtype False; inv H.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros. assert (z = Some c) by (clear - H0; inv H0; auto).
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  subst. assert (join a b c) by   (clear - H; inv H; auto).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (Some a, None, Some b, None); repeat split; try constructor; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct d as [d|].
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (z=Some d) by (clear - H0; inv H0; auto). subst z.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None, Some a, None, Some b); repeat split; try constructor; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  clear - H; inv H; auto.
  elimtype False; inv H0; inv H.
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@Some B b) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct c as [c|]. destruct d as [d|].
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@Some B d))))) *)
(* Goal: forall (z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@Some B c) (@None B) z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (z = Some a) by (clear - H; inv H; auto). subst z.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (Some c, Some d, None, None); repeat split; try constructor; eauto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  inv H0; auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  intros. assert (z = Some a) by (clear - H; inv H; auto). subst.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@Some B c)) (@join (option B) (@Join_lower B JB) ad bd (@None B))))) *)
(* Goal: forall (d z : option B) (_ : @join (option B) (@Join_lower B JB) (@Some B a) (@None B) z) (_ : @join (option B) (@Join_lower B JB) (@None B) d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (a=c) by (clear - H0; inv H0; auto). subst c.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (Some a, None, None, None); repeat split; try constructor; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (z=d) by (clear - H0; inv H0; auto). subst d.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@Some B a)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd z)))) *)
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (z = Some a) by (inv H; auto).
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  subst.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None, Some a, None, None); repeat split; try constructor; auto.
(* Goal: forall (b c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) b z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd b) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  destruct b as [b|]. destruct c as [c|]. destruct d as [d|].
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  assert (z=Some b) by (inv H; auto). subst.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None, None, Some c, Some d); repeat split; try constructor; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  inv H0; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  assert (z = Some b) by (inv H; auto); subst.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  assert (c=b) by (inv H0; auto); subst.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None, None, Some b, None); repeat split; try constructor; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@Some B b)) (and (@join (option B) (@Join_lower B JB) ac bc (@None B)) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: forall (c d z : option B) (_ : @join (option B) (@Join_lower B JB) (@None B) (@None B) z) (_ : @join (option B) (@Join_lower B JB) c d z), @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  assert (z=d) by (clear - H0; inv H0; auto). subst d.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  assert (z=Some b) by (inv H; auto). subst.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  exists (None, None, None, Some b); repeat split; try constructor; auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros. assert (z=None) by (inv H; auto).
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join A JA ac ad a) (and (@join A JA bc bd b) (and (@join A JA ac bc c) (@join A JA ad bd d)))) *)
  subst.
(* Goal: @sigT (prod (prod (prod (option B) (option B)) (option B)) (option B)) (fun x : prod (prod (prod (option B) (option B)) (option B)) (option B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (option B) (@Join_lower B JB) ac ad (@None B)) (and (@join (option B) (@Join_lower B JB) bc bd (@None B)) (and (@join (option B) (@Join_lower B JB) ac bc c) (@join (option B) (@Join_lower B JB) ad bd d)))) *)
(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  exists (None, None, None, None).
(* Goal: @join (option (@lifted A JA)) (@Join_lower (@lifted A JA) (@Join_lift A JA)) (@Some (@lifted A JA) a) (@Some (@lifted A JA) (@mk_lifted A JA b (@nonidentity_nonunit A JA PA SA CA b n))) (@Some (@lifted A JA) c) *)
  inv H0; repeat split; constructor.

(* Goal: @Cross_alg (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) *)
  intros [a Ha] [b Hb] [c Hc] [d Hd] [z Hz].
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  simpl; intros.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  unfold Cross_alg in X.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  destruct (X (fun x => a x) b c d z); auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct x as [[[s p] q] r].
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  decompose [and] y; clear y.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hs : finMap s).
(* Goal: @finMap A B s *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Ha.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option B) (s a0) (@None B) *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  specialize ( H1 a0).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H1; auto. inv H1; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hq : finMap q).
(* Goal: @finMap A B r *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hb.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  specialize ( H3 a0). inv H3; auto. rewrite H9; rewrite e; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H8; auto. inv H8.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hr : finMap r).
(* Goal: @finMap A B r *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hb.
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists x.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  intros.
(* Goal: @eq (option B) (r a0) (@None B) *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  specialize ( H3 a0).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  rewrite e in H3; auto. inv H3; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  assert (Hp : finMap p).
(* Goal: @finMap A B p *)
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  destruct Hd.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
  exists x. intros. specialize ( H5 a0). rewrite e in H5; auto. inv H5; auto.
(* Goal: @sigT (prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B)) (fun x : prod (prod (prod (fpm A B) (fpm A B)) (fpm A B)) (fpm A B) => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac ad (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) bc bd (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ac bc (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) ad bd (@exist (forall _ : A, option B) (@finMap A B) d Hd))))) *)
  exists (exist _ s Hs, exist _ p Hp, exist _ q Hq, exist _ r Hr).
(* Goal: and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) a Ha)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) b Hb)) (and (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) s Hs) (@exist (forall _ : A, option B) (@finMap A B) q Hq) (@exist (forall _ : A, option B) (@finMap A B) c Hc)) (@join (fpm A B) (Join_prop (forall _ : A, option B) (Join_pi A (fun _ : A => option B) (fun _ : A => @Join_lower B JB)) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) p Hp) (@exist (forall _ : A, option B) (@finMap A B) r Hr) (@exist (forall _ : A, option B) (@finMap A B) d Hd)))) *)
  simpl; intuition.
Qed.

Definition opposite_bij {A B} (b: bijection A B) : bijection B A :=
 Bijection _ _ (bij_g _ _ b) (bij_f _ _ b) (bij_gf _ _ b) (bij_fg _ _ b).

Lemma Cross_bij' : forall A B JA JB bij,
  @Cross_alg B JB ->
   JB =  (Join_bij A JA B bij) ->
  @Cross_alg A  JA.
Proof.
(* Goal: forall (A B : Type) (JA : Join A) (JB : Join B) (bij : bijection A B) (_ : @Cross_alg B JB) (_ : @eq (Join B) JB (Join_bij A JA B bij)), @Cross_alg A JA *)
  repeat intro. subst. unfold join, Join_bij in *.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct bij. simpl in *.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct (X (bij_f a) (bij_f b) (bij_f c) (bij_f d) (bij_f z)).
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  red. repeat rewrite bij_gf; auto.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  red. repeat rewrite bij_gf; auto.
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  destruct x as [[[s p] q] r].
(* Goal: @sigT (prod (prod (prod A A) A) A) (fun x : prod (prod (prod A A) A) A => let (p, bd) := x in let (p0, bc) := p in let (ac, ad) := p0 in and (JA ac ad a) (and (JA bc bd b) (and (JA ac bc c) (JA ad bd d)))) *)
  exists (bij_g s,bij_g p,bij_g q,bij_g r).
(* Goal: and (JA (bij_g s) (bij_g p) a) (and (JA (bij_g q) (bij_g r) b) (and (JA (bij_g s) (bij_g q) c) (JA (bij_g p) (bij_g r) d))) *)
  unfold join in y.
(* Goal: and (JA (bij_g s) (bij_g p) a) (and (JA (bij_g q) (bij_g r) b) (and (JA (bij_g s) (bij_g q) c) (JA (bij_g p) (bij_g r) d))) *)
  repeat rewrite bij_gf in y.
(* Goal: @eq (option A) (@Some A a) (@Some A a) *)
  auto.
Qed.

Definition option_bij {A B} (D: bijection A B) : bijection (option A) (option B).
 apply
 (Bijection (option A) (option B)
    (fun a => match a with Some a' => Some (bij_f _ _ D a') | None => None end)
    (fun b => match b with Some b' => Some (bij_g _ _ D b') | None => None end)).
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
 intros. destruct x; simpl; auto. rewrite bij_fg. auto.
(* Goal: forall x : option A, @eq (option A) match match x with | Some a' => @Some B (bij_f A B D a') | None => @None B end with | Some b' => @Some A (bij_g A B D b') | None => @None A end x *)
 intros. destruct x; simpl; auto. rewrite bij_gf. auto.
Defined.
