Nuprl - Pf switchable

(14steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
5. x,y,z:|E| List. P(x) P(y) composableR(E)(x,y,z) P(z)

x,y,z:A List. P(map(f;x)) P(map(f;y)) composableR(induced_event_str(E;A;f))(x,y,z) P(map(f;z))

By: Auto THEN Using [`x',map(f;x);`y',map(f;y)] BackThruSomeHyp

Generated subgoal:

1 6. x: A List
7. y: A List
8. z: A List
9. P(map(f;x))
10. P(map(f;y))
11. composableR(induced_event_str(E;A;f))(x,y,z)
composableR(E)(map(f;x),map(f;y),map(f;z))

About:

(14steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc