Init.Core

instDecidableIff = if hp : p then if hq : q then isTrue (_ : p ↔ q) else isFalse (_ : (p ↔ q) → False) else if hq : q then isFalse (_ : (p ↔ q) → False) else isTrue (_ : p ↔ q)

source

theorem if_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : α} {e : α} :

(if c then t else e) = t

source

theorem if_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : α} {e : α} :

(if c then t else e) = e

source

theorem dif_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :

dite c t e = t hc

source

theorem dif_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :

dite c t e = e hnc

source

theorem dif_eq_if (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) :

(if h : c then t else e) = if c then t else e

source

instance instDecidableIteProp {c : Prop} {t : Prop} {e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] :

Decidable (if c then t else e)

Equations

instDecidableIteProp = match dC with | isTrue hc => dT | isFalse hc => dE

source

instance instDecidableDitePropNot {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : (h : c) → Decidable (t h)] [dE : (h : ¬c) → Decidable (e h)] :

Decidable (if h : c then t h else e h)

Equations

instDecidableDitePropNot = match dC with | isTrue hc => dT hc | isFalse hc => dE hc

source

@[inline]

abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x : α) (y : α) :

Sort w

Equations

noConfusionTypeEnum f P x y = if f x = f y then P → P else P

source

@[inline]

abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x : α} {y : α} (h : x = y) :

noConfusionTypeEnum f P x y

Equations

noConfusionEnum f h = if h' : f x = f y then cast (_ : (P → P) = if f x = f y then P → P else P) fun h => h else False.elim (_ : False)

source

instance instInhabitedProp :

Inhabited Prop

Equations

instInhabitedProp = { default := True }

source

instance instInhabitedTrue :

Inhabited True

Equations

instInhabitedTrue = { default := True.intro }

source

instance instInhabitedPNonScalar :

Inhabited PNonScalar

Equations

instInhabitedPNonScalar = { default := PNonScalar.mk default }

source

instance instInhabitedNonScalar :

Inhabited NonScalar

Equations

instInhabitedNonScalar = { default := { val := default } }

source

instance instInhabitedForInStep :

{a : Type u_1} → [inst : Inhabited a] → Inhabited (ForInStep a)

Equations

instInhabitedForInStep = { default := ForInStep.done default }

source

theorem nonempty_of_exists {α : Sort u} {p : α → Prop} :

(∃ x, p x) → Nonempty α

source

class Subsingleton (α : Sort u) :

Prop

intro :: (

allEq : ∀ (a b : α), a = b

)

Instances

source

noncomputable def Subsingleton.elim {α : Sort u} [h : Subsingleton α] (a : α) (b : α) :

a = b

Equations

@Subsingleton.elim = @Subsingleton.elim.proof_1

source

noncomputable def Subsingleton.helim {α : Sort u} {β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) :

HEq a b

Equations

@Subsingleton.helim = @Subsingleton.helim.proof_1

source

noncomputable instance instSubsingleton (p : Prop) :

Subsingleton p

Equations

instSubsingleton = instSubsingleton.proof_1

source

noncomputable instance instSubsingletonDecidable (p : Prop) :

Subsingleton (Decidable p)

Equations

instSubsingletonDecidable = instSubsingletonDecidable.proof_1

source

theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :

Subsingleton (Decidable.casesOn h h₂ h₁)

source

structure Equivalence {α : Sort u} (r : α → α → Prop) :

Prop

refl : (x : α) → r x x
symm : {x y : α} → r x y → r y x
trans : {x y z : α} → r x y → r y z → r x z

source

noncomputable def emptyRelation {α : Sort u} (a₁ : α) (a₂ : α) :

Prop

Equations

emptyRelation a₁ a₂ = False

source

noncomputable def Subrelation {α : Sort u} (q : α → α → Prop) (r : α → α → Prop) :

Prop

Equations

Subrelation q r = ({x y : α} → q x y → r x y)

source

noncomputable def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) :

α → α → Prop

Equations

InvImage r f a₁ a₂ = r (f a₁) (f a₂)

source

inductive TC {α : Sort u} (r : α → α → Prop) :

α → α → Prop

base: ∀ {α : Sort u} {r : α → α → Prop} (a b : α), r a b → TC r a b
trans: ∀ {α : Sort u} {r : α → α → Prop} (a b c : α), TC r a b → TC r b c → TC r a c

source

noncomputable def Subtype.existsOfSubtype {α : Type u} {p : α → Prop} :

{ x // p x } → ∃ x, p x

Equations

@Subtype.existsOfSubtype = @Subtype.existsOfSubtype.proof_1

source

theorem Subtype.eq {α : Type u} {p : α → Prop} {a1 : { x // p x }} {a2 : { x // p x }} :

a1.val = a2.val → a1 = a2

source

theorem Subtype.eta {α : Type u} {p : α → Prop} (a : { x // p x }) (h : p a.val) :

{ val := a.val, property := h } = a

source

instance Subtype.instInhabitedSubtype {α : Type u} {p : α → Prop} {a : α} (h : p a) :

Inhabited { x // p x }

Equations

Subtype.instInhabitedSubtype h = { default := { val := a, property := h } }

source

instance Subtype.instDecidableEqSubtype {α : Type u} {p : α → Prop} [inst : DecidableEq α] :

DecidableEq { x // p x }

Equations

Subtype.instDecidableEqSubtype x x = match x with | { val := a, property := h₁ } => match x with | { val := b, property := h₂ } => if h : a = b then isTrue (_ : { val := a, property := h₁ } = { val := b, property := h₂ }) else isFalse (_ : { val := a, property := h₁ } = { val := b, property := h₂ } → False)

source

instance Sum.inhabitedLeft {α : Type u} {β : Type v} [h : Inhabited α] :

Inhabited (α ⊕ β)

Equations

Sum.inhabitedLeft = { default := Sum.inl default }

source

instance Sum.inhabitedRight {α : Type u} {β : Type v} [h : Inhabited β] :

Inhabited (α ⊕ β)

Equations

Sum.inhabitedRight = { default := Sum.inr default }

source

instance instDecidableEqSum {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] :

DecidableEq (α ⊕ β)

Equations

instDecidableEqSum a b = match a, b with | Sum.inl a, Sum.inl b => if h : a = b then isTrue (_ : Sum.inl a = Sum.inl b) else isFalse (_ : Sum.inl a = Sum.inl b → False) | Sum.inr a, Sum.inr b => if h : a = b then isTrue (_ : Sum.inr a = Sum.inr b) else isFalse (_ : Sum.inr a = Sum.inr b → False) | Sum.inr a, Sum.inl b => isFalse (_ : Sum.inr a = Sum.inl b → Sum.noConfusionType False (Sum.inr a) (Sum.inl b)) | Sum.inl a, Sum.inr b => isFalse (_ : Sum.inl a = Sum.inr b → Sum.noConfusionType False (Sum.inl a) (Sum.inr b))

source

instance instInhabitedProd {α : Type u_1} {β : Type u_2} [inst : Inhabited α] [inst : Inhabited β] :

Inhabited (α × β)

Equations

instInhabitedProd = { default := (default, default) }

source

instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] :

DecidableEq (α × β)

Equations

instDecidableEqProd x x = match x with | (a, b) => match x with | (a', b') => match decEq a a' with | isTrue e₁ => match decEq b b' with | isTrue e₂ => isTrue (_ : (a, b) = (a', b')) | isFalse n₂ => isFalse (_ : (a, b) = (a', b') → False) | isFalse n₁ => isFalse (_ : (a, b) = (a', b') → False)

source

instance instBEqProd {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : BEq β] :

BEq (α × β)

Equations

instBEqProd = { beq := fun x x_1 => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => a₁ == a₂ && b₁ == b₂ }

source

instance instLTProd {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :

LT (α × β)

Equations

instLTProd = { lt := fun s t => s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd }

source

instance prodHasDecidableLt {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : DecidableEq α] [inst : DecidableEq β] [inst : (a b : α) → Decidable (a < b)] [inst : (a b : β) → Decidable (a < b)] (s : α × β) (t : α × β) :

Decidable (s < t)

Equations

prodHasDecidableLt t s = inferInstanceAs (Decidable (t.fst < s.fst ∨ t.fst = s.fst ∧ t.snd < s.snd))

source

theorem Prod.lt_def {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] (s : α × β) (t : α × β) :

(s < t) = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)

source

theorem Prod.ext {α : Type u_1} {β : Type u_2} (p : α × β) :

(p.fst, p.snd) = p

source

def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) :

α₁ × β₁ → α₂ × β₂

Equations

Prod.map f g x = match x with | (a, b) => (f a, g b)

source

theorem ex_of_PSigma {α : Type u} {p : α → Prop} :

(x : α) ×' p x → ∃ x, p x

source

theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ : α} {a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂) (h₂ : h₁ ▸ b₁ = b₂) :

{ fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }

source

theorem PUnit.subsingleton (a : PUnit) (b : PUnit) :

a = b

source

theorem PUnit.eq_punit (a : PUnit) :

a = PUnit.unit

source

noncomputable instance instSubsingletonPUnit :

Subsingleton PUnit

Equations

instSubsingletonPUnit = (_ : Subsingleton PUnit)

source

instance instInhabitedPUnit :

Inhabited PUnit

Equations

instInhabitedPUnit = { default := PUnit.unit }

source

instance instDecidableEqPUnit :

DecidableEq PUnit

Equations

instDecidableEqPUnit a b = isTrue (_ : a = b)

source

class Setoid (α : Sort u) :

Sort (max 1 u)

r : α → α → Prop
iseqv : Equivalence r

Instances

_private.Init.Core.0.funSetoid

source

instance instHasEquiv {α : Sort u} [inst : Setoid α] :

HasEquiv α

Equations

instHasEquiv = { Equiv := Setoid.r }

source

theorem Setoid.refl {α : Sort u} [inst : Setoid α] (a : α) :

a ≈ a

source

theorem Setoid.symm {α : Sort u} [inst : Setoid α] {a : α} {b : α} (hab : a ≈ b) :

b ≈ a

source

theorem Setoid.trans {α : Sort u} [inst : Setoid α] {a : α} {b : α} {c : α} (hab : a ≈ b) (hbc : b ≈ c) :

a ≈ c

source

axiom propext {a : Prop} {b : Prop} :

∀ (a : a ↔ b), a = b

source

theorem Eq.propIntro {a : Prop} {b : Prop} (h₁ : a → b) (h₂ : (a : b) → a) :

a = b

source

instance instDecidableEqProp {p : Prop} {q : Prop} [d : Decidable (p ↔ q)] :

Decidable (p = q)

Equations

instDecidableEqProp = match d with | isTrue h => isTrue (_ : p = q) | isFalse h => isFalse (_ : p = q → False)

source

theorem Iff.subst {a : Prop} {b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) :

p b

source

axiom Quot.sound {α : Sort u} {r : α → α → Prop} {a : α} {b : α} :

∀ (a : r a b), Quot.mk r a = Quot.mk r b

source

theorem Quot.liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) (a : α) :

Quot.lift f c (Quot.mk r a) = f a

source

theorem Quot.indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : (a : α) → motive (Quot.mk r a)) (a : α) :

Quot.ind p (Quot.mk r a) = p a

source

@[inline]

abbrev Quot.liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) :

β

Equations

Quot.liftOn q f c = Quot.lift f c q

source

theorem Quot.inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r) (h : (a : α) → motive (Quot.mk r a)) :

motive q

source

theorem Quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) :

∃ a, Quot.mk r a = q

source

@[macroInline]

def Quot.indep {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (a : α) :

PSigma motive

Equations

Quot.indep f a = { fst := Quot.mk r a, snd := f a }

source

theorem Quot.indepCoherent {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (a : α) (b : α) :

∀ (a : r a b), Quot.indep f a = Quot.indep f b

source

theorem Quot.liftIndepPr1 {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (q : Quot r) :

(Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).fst = q

source

@[inline]

abbrev Quot.rec {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) (q : Quot r) :

motive q

Equations

Quot.rec f h q = Eq.ndrecOn (_ : (Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).fst = q) (Quot.lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).snd

source

@[inline]

abbrev Quot.recOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) :

motive q

Equations

Quot.recOn q f h = Quot.rec f h q

source

@[inline]

abbrev Quot.recOnSubsingleton {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :

motive q

Equations

Quot.recOnSubsingleton q f = Quot.rec (fun a => f a) (_ : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) q

source

@[inline]

abbrev Quot.hrecOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : ∀ (a b : α), r a b → HEq (f a) (f b)) :

motive q

Equations

Quot.hrecOn q f c = Quot.recOn q f (_ : ∀ (a b : α), r a b → (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b)

source

noncomputable def Quotient {α : Sort u} (s : Setoid α) :

Sort u

Equations

Quotient s = Quot Setoid.r

source

@[inline]

def Quotient.mk {α : Sort u} (s : Setoid α) (a : α) :

Quotient s

Equations

Quotient.mk s a = Quot.mk Setoid.r a

source

def Quotient.mk' {α : Sort u} [s : Setoid α] (a : α) :

Quotient s

Equations

Quotient.mk' a = Quotient.mk s a

source

noncomputable def Quotient.sound {α : Sort u} {s : Setoid α} {a : α} {b : α} :

∀ (a : a ≈ b), Quotient.mk s a = Quotient.mk s b

Equations

@Quotient.sound = @Quotient.sound.proof_1

source

@[inline]

abbrev Quotient.lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) :

(∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β

Equations

Quotient.lift f = Quot.lift f

source

theorem Quotient.ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} :

((a : α) → motive (Quotient.mk s a)) → (q : Quot Setoid.r) → motive q

source

@[inline]

abbrev Quotient.liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) :

β

Equations

Quotient.liftOn q f c = Quot.liftOn q f c

source

theorem Quotient.inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s) (h : (a : α) → motive (Quotient.mk s a)) :

motive q

source

theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) :

∃ a, Quotient.mk s a = q

source

@[inline]

def Quotient.rec {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α), a ≈ b → (_ : Quotient.mk s a = Quotient.mk s b) ▸ f a = f b) (q : Quotient s) :

motive q

Equations

Quotient.rec f h q = Quot.rec f h q

source

@[inline]

abbrev Quotient.recOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α), a ≈ b → (_ : Quotient.mk s a = Quotient.mk s b) ▸ f a = f b) :

motive q

Equations

Quotient.recOn q f h = Quot.recOn q f h

source

@[inline]

abbrev Quotient.recOnSubsingleton {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))] (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) :

motive q

Equations

Quotient.recOnSubsingleton q f = Quot.recOnSubsingleton q f

source

@[inline]

abbrev Quotient.hrecOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (c : ∀ (a b : α), a ≈ b → HEq (f a) (f b)) :

motive q

Equations

Quotient.hrecOn q f c = Quot.hrecOn q f c

source

@[inline]

abbrev Quotient.lift₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :

φ

Equations

Quotient.lift₂ f c q₁ q₂ = Quotient.lift (fun a₁ => Quotient.lift (f a₁) (_ : ∀ (a b : β), a ≈ b → f a₁ a = f a₁ b) q₂) (_ : ∀ (a b : α), a ≈ b → (fun a₁ => Quotient.lift (f a₁) (fun a b => c a₁ a a₁ b (_ : a₁ ≈ a₁)) q₂) a = (fun a₁ => Quotient.lift (f a₁) (fun a b => c a₁ a a₁ b (_ : a₁ ≈ a₁)) q₂) b) q₁

source

@[inline]

abbrev Quotient.liftOn₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :

φ

Equations

Quotient.liftOn₂ q₁ q₂ f c = Quotient.lift₂ f c q₁ q₂

source

theorem Quotient.ind₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :

motive q₁ q₂

source

theorem Quotient.inductionOn₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :

motive q₁ q₂

source

theorem Quotient.inductionOn₃ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ} {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : (a : α) → (b : β) → (c : φ) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)) :

motive q₁ q₂ q₃

source

theorem Quotient.exact {α : Sort u} {s : Setoid α} {a : α} {b : α} :

∀ (a : Quotient.mk s a = Quotient.mk s b), a ≈ b

source

@[inline]

abbrev Quotient.recOnSubsingleton₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC} [s : ∀ (a : α) (b : β), Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (g : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :

motive q₁ q₂

Equations