Skip to content

Instantly share code, notes, and snippets.

Last active Oct 13, 2021
What would you like to do?
attribute[simp]in_hd in_tl
def P(x:A)(l m):x~l++m↔x~l∨x~m:=by induction l;split;intro;repeat{finish<|>cases ᾰ<|>cases l_ih.1
ᾰ_ᾰ}def R(x:A)(l)(i:x~l):x~rev l:=by induction i;simp[P];left;tauto
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment