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

Theorem

relations.RC_reflexive

Statement

∀ R, reflexive (RC R)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem RC_reflexive : forall A, forall (R:(A -> A -> Prop)), reflexive (A) (RC (A) R).



Matita-Jumb
Statement

theorem RC_reflexive : \forall A. \forall (R:A -> A -> Prop). (reflexive) (A) ((RC) (A) R).



Lean-jumb
Statement

theorem RC_reflexive : forall (A : Type) , forall (R:(A) -> (A) -> Prop) , ((relations.reflexive) (A)) (((relations.RC) (A)) (R)).



PVS-jumb

Statement

RC_reflexive [A:TYPE+] : LEMMA (FORALL(R:[A -> [A -> bool]]):relations_sttfa.reflexive[A](relations_sttfa.RC[A](R)))



OpenTheory

Printing for OpenTheory is not working at the moment.