importproveitfromproveit.logic.booleans.implicationimportfalse_implies_truetheory=proveit.Theory()# the theorem's theory
In [2]:
%proving implies_f_t
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of implies_f_t: (see dependencies)
implies_f_t may now be readily provable (assuming required theorems are usable). Simply execute "%qed".
In [3]:
%qed
proveit.logic.booleans.implication.implies_f_t has been proven.