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

At: rel-graph functionality 2 4
1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
5. b: {p:(TT)| R2(1of(p),2of(p)) }
a:{p:(TT)| R1(1of(p),2of(p)) }. a = b {p:(TT)| R2(1of(p),2of(p)) }
By:
InstConcl [b]
THEN
ParallelOp -1
THEN
EasyHyp
Generated subgoals:

None

About:
productsetfunctionuniverseequalpropallexists

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