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

Axiom

connectives.or_introl

Statement

∀ A B, A ⇒ A ∨ B

Main Dependencies
constant
connectives.Or
Theory
constant
connectives.Or
Coq-Jumb
Statement

Axiom or_introl : forall (A:Prop), forall (B:Prop), A -> Or A B


Matita-Jumb
Statement

axiom or_introl : \forall (A:Prop). \forall (B:Prop). (A) -> (Or) A B


Lean-jumb
Statement

axiom or_introl : forall (A:Prop) , forall (B:Prop) , (A) -> (((connectives.Or) ) (A)) (B)


PVS-jumb
Statement

or_introl : AXIOM (FORALL(A:bool):(FORALL(B:bool):(A => connectives_sttfa.sttfa_Or(A)(B))))


OpenTheory

Printing for OpenTheory is not working at the moment.