* Initial invocation: - Patience on me to gain peace and perfection! -
*)
-include "ground_2/lib/relations.ma".
+include "ground/lib/relations.ma".
include "static_2/notation/functions/item0_0.ma".
include "static_2/notation/functions/snitem2_2.ma".
]
]
qed-.
+
+lemma is_apear_dec (B) (X): Decidable (∃A. ②B.A = X).
+#B * [| #X #A ]
+[| elim (eq_aarity_dec X B) #HX ]
+[| /3 width=2 by ex_intro, or_introl/ ]
+@or_intror * #A #H destruct
+/2 width=1 by/
+qed-.