theorem univ_fin2 : Finset.univ = {0, 1}

theorem notc {c x y : Fin 2} : x ≠ c → y ≠ c → x = y

theorem not0_eq1 {x : Fin 2} : x ≠ 0 ↔ x = 1