kdrag.kernel.andI

kdrag.kernel.andI(a: Proof, b: Proof) → Proof

Prove an and from two proofs of its conjuncts.

>>> a, b = smt.Bools("a b")
>>> pa = axiom(a)
>>> pb = axiom(b)
>>> andI(pa, pb)
|- And(a, b)

Parameters:

• a (Proof)

• b (Proof)

Return type:

Proof