Theorem: weakly_confluent_does_not_imply_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∃ A R, weakly_confluent R ∧ ¬confluent R
Tactic:
exists X, RX
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX ∧ ¬confluent RX

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX ∧ ¬confluent RX
Tactic:
constructor
State after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
. intros x y z r_x_y r_x_z
  simp [*] at r_x_y
  simp [*] at r_x_z
  cases r_x_y <;> cases r_x_z <;> simp [*] at *
  . exists X.a; repeat constructor
  . exists X.a; try constructor
    . constructor
    . simp [*]; constructor; simp [RX]
      . left; trivial
      . constructor; simp [RX]; left; trivial; constructor
  . exists X.a; simp [*]; constructor
    . repeat (constructor; simp [RX]; left; trivial)
      constructor
    . constructor
  . case inr h1 h2 =>
    cases h1 <;> cases h2 <;> simp [*] at *
    . exists X.c; repeat constructor
    . case inr h1 h2 =>
      cases h1 <;> cases h2 <;> simp [*] at *
      . exists X.b; repeat constructor
      . exists X.d; constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
        . constructor
      . exists X.d; constructor
        . constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
      . exists X.d; repeat constructor
State after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
. intros h
  apply not_joins_a_d
  apply h
  exists X.b; constructor
  . constructor
    simp [RX]
    left; trivial
    constructor
  . constructor
    simp [RX]
    right; trivial
    constructor
    . simp [RX]; right; trivial
    . constructor
State after:
no goals

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX
Tactic:
intros x y z r_x_y r_x_z
State after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z
Tactic:
simp [*] at r_x_y
State after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : RX x z
⊢ joins RX y z

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : RX x z
⊢ joins RX y z
Tactic:
simp [*] at r_x_z
State after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : x = X.b ∧ z = X.a ∨ x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins RX y z

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : x = X.b ∧ z = X.a ∨ x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins RX y z
Tactic:
cases r_x_y <;> cases r_x_z <;> simp [*] at *
State after:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; repeat constructor
State after:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; try constructor
  . constructor
  . simp [*]; constructor; simp [RX]
    . left; trivial
    . constructor; simp [RX]; left; trivial; constructor
State after:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; simp [*]; constructor
  . repeat (constructor; simp [RX]; left; trivial)
    constructor
  . constructor
State after:
case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. case inr h1 h2 =>
  cases h1 <;> cases h2 <;> simp [*] at *
  . exists X.c; repeat constructor
  . case inr h1 h2 =>
    cases h1 <;> cases h2 <;> simp [*] at *
    . exists X.b; repeat constructor
    . exists X.d; constructor
      . constructor; simp [RX]; right; trivial
        constructor; simp [RX]; right; trivial
        constructor
      . constructor
    . exists X.d; constructor
      . constructor
      . constructor; simp [RX]; right; trivial
        constructor; simp [RX]; right; trivial
        constructor
    . exists X.d; repeat constructor
State after:
no goals

State before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
exists X.a
State after:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
repeat constructor
State after:
no goals

State before:
case left.inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
no goals

State before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z
Tactic:
exists X.a
State after:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a

State before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
try constructor
State after:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a

State before:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
. constructor
State after:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a

State before:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
. simp [*]; constructor; simp [RX]
  . left; trivial
  . constructor; simp [RX]; left; trivial; constructor
State after:
no goals

State before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
constructor
State after:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a

State before:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
no goals

State before:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
simp [*]
State after:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a

State before:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a
Tactic:
constructor
State after:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X.c = X.b ∧ ?left.inl.inr.right.b = X.a ∨
    X.c = X.b ∧ ?left.inl.inr.right.b = X.c ∨
      X.c = X.c ∧ ?left.inl.inr.right.b = X.b ∨ X.c = X.c ∧ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X

State before:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X.c = X.b ∧ ?left.inl.inr.right.b = X.a ∨
    X.c = X.b ∧ ?left.inl.inr.right.b = X.c ∨
      X.c = X.c ∧ ?left.inl.inr.right.b = X.b ∨ X.c = X.c ∧ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X
Tactic:
simp [RX]
State after:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X

State before:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X
Tactic:
. left; trivial
State after:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.a

State before:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.a
Tactic:
. constructor; simp [RX]; left; trivial; constructor
State after:
no goals

State before:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d
Tactic:
left
State after:
case left.inl.inr.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.b = X.b

State before:
case left.inl.inr.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.b = X.b
Tactic:
trivial
State after:
no goals

State before:
case left.inl.inr.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.a
Tactic:
constructor
State after:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X.b = X.b ∧ ?left.inl.inr.right.a.b = X.a ∨
    X.b = X.b ∧ ?left.inl.inr.right.a.b = X.c ∨
      X.b = X.c ∧ ?left.inl.inr.right.a.b = X.b ∨ X.b = X.c ∧ ?left.inl.inr.right.a.b = X.d

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X

State before:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X.b = X.b ∧ ?left.inl.inr.right.a.b = X.a ∨
    X.b = X.b ∧ ?left.inl.inr.right.a.b = X.c ∨
      X.b = X.c ∧ ?left.inl.inr.right.a.b = X.b ∨ X.b = X.c ∧ ?left.inl.inr.right.a.b = X.d

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X
Tactic:
simp [RX]
State after:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.a.b = X.a ∨ ?left.inl.inr.right.a.b = X.c

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X

State before:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.a.b = X.a ∨ ?left.inl.inr.right.a.b = X.c

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X
Tactic:
left
State after:
case left.inl.inr.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.a.b = X.a

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X

State before:
case left.inl.inr.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ ?left.inl.inr.right.a.b = X.a

case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ X
Tactic:
trivial
State after:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inl.inr.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
no goals

State before:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a
Tactic:
exists X.a
State after:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
simp [*]
State after:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
case left.inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a

case left.inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a

case left.inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
. repeat (constructor; simp [RX]; left; trivial)
  constructor
State after:
case left.inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
. constructor
State after:
no goals

State before:
case left.inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.a
Tactic:
repeat (constructor; simp [RX]; left; trivial)
State after:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
no goals

State before:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
(constructor; simp [RX]; left; trivial)
State after:
no goals

State before:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X.b = X.b ∧ ?left.inr.inl.left.a.b = X.a ∨
    X.b = X.b ∧ ?left.inr.inl.left.a.b = X.c ∨
      X.b = X.c ∧ ?left.inr.inl.left.a.b = X.b ∨ X.b = X.c ∧ ?left.inr.inl.left.a.b = X.d

case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X
Tactic:
simp [RX]
State after:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ ?left.inr.inl.left.a.b = X.a ∨ ?left.inr.inl.left.a.b = X.c

case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X

State before:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ ?left.inr.inl.left.a.b = X.a ∨ ?left.inr.inl.left.a.b = X.c

case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X
Tactic:
left
State after:
case left.inr.inl.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ ?left.inr.inl.left.a.b = X.a

case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X

State before:
case left.inr.inl.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ ?left.inr.inl.left.a.b = X.a

case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ X
Tactic:
trivial
State after:
case left.inr.inl.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

State before:
case left.inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
case inr h1 h2 =>
cases h1 <;> cases h2 <;> simp [*] at *
. exists X.c; repeat constructor
. case inr h1 h2 =>
  cases h1 <;> cases h2 <;> simp [*] at *
  . exists X.b; repeat constructor
  . exists X.d; constructor
    . constructor; simp [RX]; right; trivial
      constructor; simp [RX]; right; trivial
      constructor
    . constructor
  . exists X.d; constructor
    . constructor
    . constructor; simp [RX]; right; trivial
      constructor; simp [RX]; right; trivial
      constructor
  . exists X.d; repeat constructor
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
cases h1 <;> cases h2 <;> simp [*] at *
State after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.c; repeat constructor
State after:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z

State before:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. case inr h1 h2 =>
  cases h1 <;> cases h2 <;> simp [*] at *
  . exists X.b; repeat constructor
  . exists X.d; constructor
    . constructor; simp [RX]; right; trivial
      constructor; simp [RX]; right; trivial
      constructor
    . constructor
  . exists X.d; constructor
    . constructor
    . constructor; simp [RX]; right; trivial
      constructor; simp [RX]; right; trivial
      constructor
  . exists X.d; repeat constructor
State after:
no goals

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c
Tactic:
exists X.c
State after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c
Tactic:
repeat constructor
State after:
no goals

State before:
case inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.c
Tactic:
constructor
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
case inr h1 h2 =>
cases h1 <;> cases h2 <;> simp [*] at *
. exists X.b; repeat constructor
. exists X.d; constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
  . constructor
. exists X.d; constructor
  . constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
. exists X.d; repeat constructor
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
cases h1 <;> cases h2 <;> simp [*] at *
State after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b

case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b

case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. exists X.b; repeat constructor
State after:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. exists X.d; constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
  . constructor
State after:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. exists X.d; constructor
  . constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
State after:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. exists X.d; repeat constructor
State after:
no goals

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b
Tactic:
exists X.b
State after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b

State before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b
Tactic:
repeat constructor
State after:
no goals

State before:
case inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.b
Tactic:
constructor
State after:
no goals

State before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
exists X.d
State after:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. constructor; simp [RX]; right; trivial
  constructor; simp [RX]; right; trivial
  constructor
State after:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
. constructor
State after:
no goals

State before:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
constructor
State after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.b = X.b ∧ ?inl.inr.left.b = X.a ∨
    X.b = X.b ∧ ?inl.inr.left.b = X.c ∨ X.b = X.c ∧ ?inl.inr.left.b = X.b ∨ X.b = X.c ∧ ?inl.inr.left.b = X.d

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.b = X.b ∧ ?inl.inr.left.b = X.a ∨
    X.b = X.b ∧ ?inl.inr.left.b = X.c ∨ X.b = X.c ∧ ?inl.inr.left.b = X.b ∨ X.b = X.c ∧ ?inl.inr.left.b = X.d

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
simp [RX]
State after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.a ∨ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.a ∨ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
right
State after:
case inl.inr.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
trivial
State after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.d

State before:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.d
Tactic:
constructor
State after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.c = X.b ∧ ?inl.inr.left.a.b = X.a ∨
    X.c = X.b ∧ ?inl.inr.left.a.b = X.c ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.b ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.c = X.b ∧ ?inl.inr.left.a.b = X.a ∨
    X.c = X.b ∧ ?inl.inr.left.a.b = X.c ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.b ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
simp [RX]
State after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.b ∨ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.b ∨ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
right
State after:
case inl.inr.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X

State before:
case inl.inr.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
trivial
State after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
no goals

State before:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
no goals

State before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.b
Tactic:
exists X.d
State after:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

State before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
constructor
State after:
case inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

State before:
case inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
. constructor
State after:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d

State before:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
. constructor; simp [RX]; right; trivial
  constructor; simp [RX]; right; trivial
  constructor
State after:
no goals

State before:
case inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
no goals

State before:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.b X.d
Tactic:
constructor
State after:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X.b = X.b ∧ ?inr.inl.right.b = X.a ∨
    X.b = X.b ∧ ?inr.inl.right.b = X.c ∨ X.b = X.c ∧ ?inr.inl.right.b = X.b ∨ X.b = X.c ∧ ?inr.inl.right.b = X.d

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X.b = X.b ∧ ?inr.inl.right.b = X.a ∨
    X.b = X.b ∧ ?inr.inl.right.b = X.c ∨ X.b = X.c ∧ ?inr.inl.right.b = X.b ∨ X.b = X.c ∧ ?inr.inl.right.b = X.d

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
simp [RX]
State after:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.b = X.a ∨ ?inr.inl.right.b = X.c

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.b = X.a ∨ ?inr.inl.right.b = X.c

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
right
State after:
case inr.inl.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.b = X.c

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.b = X.c

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
trivial
State after:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.d

State before:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.c X.d
Tactic:
constructor
State after:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X.c = X.b ∧ ?inr.inl.right.a.b = X.a ∨
    X.c = X.b ∧ ?inr.inl.right.a.b = X.c ∨ X.c = X.c ∧ ?inr.inl.right.a.b = X.b ∨ X.c = X.c ∧ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X.c = X.b ∧ ?inr.inl.right.a.b = X.a ∨
    X.c = X.b ∧ ?inr.inl.right.a.b = X.c ∨ X.c = X.c ∧ ?inr.inl.right.a.b = X.b ∨ X.c = X.c ∧ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
simp [RX]
State after:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.a.b = X.b ∨ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.a.b = X.b ∨ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
right
State after:
case inr.inl.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X

State before:
case inr.inl.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ ?inr.inl.right.a.b = X.d

case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d)
    ?inr.inl.right.a.b X.d

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
trivial
State after:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inr.inl.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
no goals

State before:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
exists X.d
State after:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d

State before:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
repeat constructor
State after:
no goals

State before:
case inr.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.d
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.d X.d
Tactic:
constructor
State after:
no goals

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
intros h
State after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ False

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ False
Tactic:
apply not_joins_a_d
State after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ joins RX X.a X.d

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ joins RX X.a X.d
Tactic:
apply h
State after:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ wedge RX X.a X.d

State before:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ wedge RX X.a X.d
Tactic:
exists X.b
State after:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a ∧ refl_trans_clos RX X.b X.d

State before:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a ∧ refl_trans_clos RX X.b X.d
Tactic:
constructor
State after:
case right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a

case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d

State before:
case right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a

case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Tactic:
. constructor
  simp [RX]
  left; trivial
  constructor
State after:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d

State before:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Tactic:
. constructor
  simp [RX]
  right; trivial
  constructor
  . simp [RX]; right; trivial
  . constructor
State after:
no goals

State before:
case right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a
Tactic:
constructor
State after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.left.b

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.left.b

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
simp [RX]
State after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a ∨ ?right.a.left.b = X.c

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a ∨ ?right.a.left.b = X.c

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
left
State after:
case right.a.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
trivial
State after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.a X.a

State before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.a X.a
Tactic:
constructor
State after:
no goals

State before:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Tactic:
constructor
State after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.right.b

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.right.b

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
simp [RX]
State after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.a ∨ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.a ∨ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
right
State after:
case right.a.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
trivial
State after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.c X.d

State before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.c X.d
Tactic:
constructor
State after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b

case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.a.b X.d

case right.a.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X

State before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b

case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.a.b X.d

case right.a.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
. simp [RX]; right; trivial
State after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d

State before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d
Tactic:
. constructor
State after:
no goals

State before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b
Tactic:
simp [RX]
State after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.b ∨ ?right.a.right.a.b = X.d

State before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.b ∨ ?right.a.right.a.b = X.d
Tactic:
right
State after:
case right.a.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.d

State before:
case right.a.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.d
Tactic:
trivial
State after:
no goals

State before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d
Tactic:
constructor
State after:
no goals