(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/connectives2".
-
include "higher_order_defs/relations.ma".
theorem reflexive_iff: reflexive ? iff.
elim H1;
split;
intro;
- autobatch.
+ autobatch depth=3.
qed.