nth_le with different le

Stream: Is there code for X?

[Chase Norman]

Is there a way to prove that list.nth_le l i a = list.nth_le l i b for distinct le proofs a and b? I'm failing to accomplish a simp_rw because of this distinction. Alternatively, is there a way to prove the inhabited type-class in tactic mode using a witness element? My trouble arises from not being able to express l.head' in terms of list.nth_le l 0 _.

[Bhavik Mehta]

I think rfl should work for the first question

[Mario Carneiro]

for the second:

import data.list.basic

namespace list
variables {α : Type*}
lemma nth_zero (l : list α) : l.nth 0 = l.head' := by cases l; refl
end list

example {α} (l : list α) (h) : l.head' = some (l.nth_le 0 h) :=
by rw [← list.nth_zero, list.nth_le_nth]