Logic.v 証明オブジェクトがどんなかたちになるかについて、 全然イメージが湧かない。 あいかわらずレバガチャ状態ではある。 Theorem or_distributes_over_and_2 : forall P Q R : Prop, (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).とか。scriptモードでも、…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。