(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: rel-graph functionality 2 3
1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
5. a1: {p:(TT)| R1(1of(p),2of(p)) }
6. a2: {p:(TT)| R1(1of(p),2of(p)) }
a2 {p:(TT)| R2(1of(p),2of(p)) }
By:
ParallelOp -1
THEN
EasyHyp
Generated subgoals:

None

About:
productsetfunctionuniversememberpropall

(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc