/\^._.^/\ BATT /\^._.^/\
-- Our beloved identity id : {A : Type} → (x : A) → A id x = x
Clear
Send