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

Axiom

connectives.conj

Statement

∀ A B, A ⇒ B ⇒ A ∧ B

Main Dependencies
Theory

Coq-Jumb
Statement

Axiom conj : forall (A:Prop), forall (B:Prop), A -> B -> And A B



Matita-Jumb
Statement

axiom conj : \forall (A:Prop). \forall (B:Prop). (A) -> (B) -> (And) A B



Lean-jumb
Statement

axiom conj : forall (A:Prop) , forall (B:Prop) , (A) -> (B) -> (((connectives.And) ) (A)) (B)



PVS-jumb

Statement

conj : AXIOM (FORALL(A:bool):(FORALL(B:bool):(A => (B => connectives_sttfa.sttfa_And(A)(B)))))



OpenTheory

Printing for OpenTheory is not working at the moment.