Skip to content

Instantly share code, notes, and snippets.

@kmill
Last active Oct 13, 2021
Embed
What would you like to do?
infix`~`:=is_in
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
-- https://codegolf.stackexchange.com/questions/236235/lean-golf-list-game-lv2-is-in-append-is-in-rev
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment