mathlib3 documentation

tactic.converter.binders

@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def old_conv.has_coe (α : Type) :
meta def old_conv.propext' {α : Type} (c : old_conv α) :
meta def old_conv.apply (pr : expr) :
meta structure binder_eq_elim  :
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