// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

logic.absurd

Statement

∀ A, A ⇒ ¬A ⇒ False

Main Dependencies
Theory
Coq-Jumb
Statement

Theorem absurd : forall (A:Prop), A -> (connectives.Not A) -> connectives.False.


Matita-Jumb
Statement

theorem absurd : \forall (A:Prop). (A) -> ((Not) A) -> (False) .


Lean-jumb
Statement

theorem absurd : forall (A:Prop) , (A) -> (((connectives.Not) ) (A)) -> (connectives.False) .


PVS-jumb
Statement

absurd : LEMMA (FORALL(A:bool):(A => (connectives_sttfa_th.sttfa_Not(A) => connectives_sttfa_th.sttfa_False)))


OpenTheory

Printing for OpenTheory is not working at the moment.