mathlib documentation

tactic.converter.binders

@[instance]

@[instance]
meta def old_conv.has_coe (α : Type) :

meta def old_conv.propext' {α : Type} :
old_conv αold_conv α

meta structure binder_eq_elim  :
Type

theorem exists_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∃ (a' : α) (h : a' = a), p a' h) p a rfl

theorem exists_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∃ (a' : α) (h : a = a'), p a' h) p a rfl

theorem forall_comm {α : Sort u} {β : Sort v} (p : α → β → Prop) :
(∀ (a : α) (b : β), p a b) ∀ (b : β) (a : α), p a b

theorem forall_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∀ (a' : α) (h : a' = a), p a' h) p a rfl

theorem forall_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∀ (a' : α) (h : a = a'), p a' h) p a rfl