proposition: Theorem nand_comm : forall (P Q : Prop), nand P Q <-> nand Q P.
proof: Proof. intros P Q. split. - intros H. destruct H. apply stroke; assumption. - intros H. destruct H. apply stroke; assumption. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)