α : Type u_1
β : Type ?u.1433
γ : Type ?u.1436
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
α : Type u_1
β : Type ?u.1433
γ : Type ?u.1436
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
have t : od = pd := propext H1
case refl
α : Type u_1
β : Type ?u.1433
γ : Type ?u.1436
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := od, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
α : Type u_1
β : Type ?u.1433
γ : Type ?u.1436
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
cases t
no goals
case refl
α : Type u_1
β : Type ?u.1433
γ : Type ?u.1436
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := od, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
rw [show o = p from funext fun p => H2 p p]