Nuprl - Pf eq_dequiv_equiv

PrintForm Definitions mb structures Sections GenAutomata Doc

At: eq dequiv equiv

E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2)

By: Auto THEN Unfolds [`carrier`;`eq_dequiv`] 0 THEN RepeatFor 3 ((Analyze -1) THEN (Reduce 0)) THEN Trivial

Generated subgoals:

None

About:

PrintForm Definitions mb structures Sections GenAutomata Doc