no goals
α✝ : Type ?u.47232
β : Type ?u.47235
R S T : α✝ → α✝ → Prop
a : α✝
l : List α✝
α : Type u_1
r : α → α → Prop
x : α
hx : r x x
⊢ Pairwise r (replicate 0 x)
simp
no goals
α✝ : Type ?u.47232
β : Type ?u.47235
R S T : α✝ → α✝ → Prop
a : α✝
l : List α✝
α : Type u_1
r : α → α → Prop
x : α
hx : r x x
n : ℕ
⊢ Pairwise r (replicate (n + 1) x)
simp only [replicate, add_eq, add_zero, pairwise_cons, mem_replicate, ne_eq,
and_imp, forall_eq_apply_imp_iff', hx, implies_true, pairwise_replicate hx n, and_self]