sep : String
escape : Bool
m n : Name
⊢ Name.beq m n = true ↔ m = n
sep : String
escape : Bool
m n : Name
⊢ (m == n) = true ↔ m = n
show m.beq n ↔ _
no goals
sep : String
escape : Bool
m n : Name
⊢ Name.beq m n = true ↔ m = n
induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]