ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 Coq の解説記事を書くために勉強しています。 (1): forall A B: Prop, (A->B) -> A -> B. CoqIDEのつかいかた。forall と -> の証明。 (2): forall A B: Prop, ~(A ∨ B) -> (~A ∧ ~…