IV. Logic and proofs

4. The objective of a demonstration is then to use the preceding rules to have no more proposition to demonstrate:

let proven ((hs,ps):Seq) : bool = (ps=[]);;

proven s3;; // = ???

Nb. "Qed" = Qod es desmonstratum - "ce qu'il fallait démontrer"

5 - 12