def and_intro

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/logic.bend:33

import Base

33def and_intro(a: Bool, b: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}) -> {Bool.and(a, b) == True{} : Bool}:
34  %Equal.sym(Bool, a, True{}, ea) : {Bool.and(_, b) == True{} : Bool}
35  eb