Nuprl - Pf member st app

PrintForm Definitions mb automata 2 Sections GenAutomata Doc

c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)

By: Unfold `st_app` 0 THEN RW ColMemberC 0 THEN RWW "member_st_app1" 0 THEN RWW "assert_st_eq" 0 THEN ExRepD THEN Repeat (AutoInstConcl []) THEN AllHyps (i.AllHyps (j.(HypSubst i j) THEN Trivial))

Generated subgoals:

None

About:

PrintForm Definitions mb automata 2 Sections GenAutomata Doc