Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.omega.Omega.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.PropositionalLogic.Syntax.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Class PropositionalVariables: Type := {
  Var: Type
}.

Inductive expr {Sigma: PropositionalVariables}: Type :=
  | andp : expr -> expr -> expr
  | orp : expr -> expr -> expr
  | impp : expr -> expr -> expr
  | falsep : expr
  | varp : Var -> expr.

Arguments expr Sigma: clear implicits.

Instance L {Sigma: PropositionalVariables}: Language :=
  Build_Language (expr Sigma).

Instance minL {Sigma: PropositionalVariables}: MinimunLanguage L :=
  Build_MinimunLanguage L impp.

Instance pL {Sigma: PropositionalVariables}: PropositionalLanguage L :=
  Build_PropositionalLanguage L andp orp falsep.

Definition rank {Sigma: PropositionalVariables}: expr Sigma -> nat :=
  fix rank (x: expr Sigma): nat :=
    match x with
    | andp y z => 1 + rank y + rank z
    | orp y z => 1 + rank y + rank z
    | impp y z => 1 + rank y + rank z
    | falsep => 0
    | varp p => 0
    end.

Definition formula_countable: forall {Sigma}, Countable Var -> Countable (expr Sigma).
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
  intros.
(* Goal: Countable (expr Sigma) *)
  assert (forall n, Countable (sig (fun x: expr Sigma => rank x <= n))).
  + induction n.
    - apply (@bijection_Countable _ (Var + unit)%type); [| solve_Countable].
(* Goal: bijection (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O)) (sum (@Var Sigma) unit) *)
      apply bijection_sym.
      apply (FBuild_bijection _ _ (fun x =>
               match x with
               | inl p => exist (fun x: expr Sigma => rank x <= 0) (varp p) (le_n 0)
               | inr _ => exist (fun x: expr Sigma => rank x <= 0) falsep (le_n 0)
               end)).
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
      * hnf; intros.
(* Goal: @eq (sum (@Var Sigma) unit) a1 a2 *)
        destruct a1 as [? | []], a2 as [? | []]; inversion H; auto.
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
      * hnf; intros.
(* Goal: @ex (sum (@Var Sigma) unit) (fun a : sum (@Var Sigma) unit => @eq (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O)) match a with | inl p => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma p) (le_n O) | inr y => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@falsep Sigma) (le_n O) end b) *)
        destruct b as [[] HH]; try solve [inversion HH].
(* Goal: @ex (sum (@Var Sigma) unit) (fun a : sum (@Var Sigma) unit => @eq (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O)) match a with | inl p => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma p) (le_n O) | inr y => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@falsep Sigma) (le_n O) end (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@falsep Sigma) HH)) *)
(* Goal: @ex (sum (@Var Sigma) unit) (fun a : sum (@Var Sigma) unit => @eq (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O)) match a with | inl p => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma p) (le_n O) | inr y => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@falsep Sigma) (le_n O) end (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma v) HH)) *)
        1: exists (inr tt); eauto; f_equal; apply proof_irrelevance.
(* Goal: @ex (sum (@Var Sigma) unit) (fun a : sum (@Var Sigma) unit => @eq (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O)) match a with | inl p => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma p) (le_n O) | inr y => @exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@falsep Sigma) (le_n O) end (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) O) (@varp Sigma v) HH)) *)
        1: exists (inl v); eauto; f_equal; apply proof_irrelevance.
    - set (s := sig (fun x: expr Sigma => rank x <= n)).
      apply (@injection_Countable _ (s * s + s * s + s * s + unit + Var)%type); [| solve_Countable].

      apply (Build_injection _ _ (fun x y =>
        match y with
        | inl (inl (inl (inl (exist _ y _, exist _ z _)))) => proj1_sig x = andp y z
        | inl (inl (inl (inr (exist _ y _, exist _ z _)))) => proj1_sig x = orp y z
        | inl (inl (inr (exist _ y _, exist _ z _))) => proj1_sig x = impp y z
        | inl (inr _) => proj1_sig x = falsep
        | inr p => proj1_sig x = varp p
        end)).
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
      * hnf; intros.
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) a) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) a) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) a) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) a) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) a) (@varp Sigma p) end) *)
        destruct a as [[y z | y z | y z | | p] ?H].
        (* 1 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega.
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@andp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@andp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@andp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@andp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@andp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@falsep Sigma) | inr p0 => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@varp Sigma p0) end) *)
                exists (inl (inl (inl (inl (exist _ y H0, exist _ z H1))))); auto.
        (* 2 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega.
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@orp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@falsep Sigma) | inr p0 => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@varp Sigma p0) end) *)
                exists (inl (inl (inl (inr (exist _ y H0, exist _ z H1))))); auto.
        (* 3 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega.
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@andp Sigma y6 z0) | inl (inl (inl (inr (pair (exist _ y6 y7 as y4) (exist _ z0 y8 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@orp Sigma y6 z0) | inl (inl (inr (pair (exist _ y5 y6 as y3) (exist _ z0 y7 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@impp Sigma y5 z0) | inl (inr y1 as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@impp Sigma y z) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@falsep Sigma) | inr p => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@falsep Sigma) H)) (@varp Sigma p) end) *)
(* Goal: @ex (sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma)) (fun b : sum (sum (sum (sum (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) (prod (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)) (@sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n)))) unit) (@Var Sigma) => match b with | inl (inl (inl (inl (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@andp Sigma y z) | inl (inl (inl (inr (pair (exist _ y y6 as y4) (exist _ z y7 as y5) as y3) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@orp Sigma y z) | inl (inl (inr (pair (exist _ y y5 as y3) (exist _ z y6 as y4) as y2) as y1) as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@impp Sigma y z) | inl (inr y as y0) => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@falsep Sigma) | inr p0 => @eq (expr Sigma) (@proj1_sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@exist (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) (S n)) (@varp Sigma p) H)) (@varp Sigma p0) end) *)
                exists (inl (inl (inr (exist _ y H0, exist _ z H1)))); auto.
        (* 4 *) exists (inl (inr tt)); auto.
        (* 5 *) exists (inr p); auto.
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
      * hnf; intros.
        destruct a as [[y z | y z | y z | | p] ?H];
        destruct b1 as [[[[[[y1 ?H] [z1 ?H]] | [[y1 ?H] [z1 ?H]]] | [[y1 ?H] [z1 ?H]]] |] | p1]; try solve [inversion H];
        destruct b2 as [[[[[[y2 ?H] [z2 ?H]] | [[y2 ?H] [z2 ?H]]] | [[y2 ?H] [z2 ?H]]] |] | p2]; try solve [inversion H0].
        (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 4 *) destruct u, u0; auto.
        (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
      * hnf; intros.
        destruct b as [[[[[[y ?H] [z ?H]] | [[y ?H] [z ?H]]] | [[y ?H] [z ?H]]] |] | p];
        destruct a1 as [[y1 z1 | y1 z1 | y1 z1 | | p1] ?H]; try solve [inversion H];
        destruct a2 as [[y2 z2 | y2 z2 | y2 z2 | | p2] ?H]; try solve [inversion H0].
        (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
        (* 4 *) f_equal; apply proof_irrelevance.
        (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance.
  + apply (@injection_Countable _ (sigT (fun n => sig (fun x: expr Sigma => rank x <= n)))); [| solve_Countable; auto].
(* Goal: injection (expr Sigma) (@sigT nat (fun n : nat => @sig (expr Sigma) (fun x : expr Sigma => le (@rank Sigma x) n))) *)
    apply (FBuild_injection _ _ (fun x0 => existT (fun n => sig (fun x => rank x <= n)) (rank x0) (exist (fun x => rank x <= rank x0) x0 (le_n (rank x0))))).
(* Goal: forall (Sigma : PropositionalVariables) (_ : Countable (@Var Sigma)), Countable (expr Sigma) *)
    hnf; intros.
(* Goal: @eq (expr Sigma) a1 a2 *)
    simpl in H.
(* Goal: @eq (expr Sigma) a1 a2 *)
    inversion H; auto.
Qed. (* 20 seconds *)

