Nuprl - Proof: union cardinality1 1

1. k1:
2. k2:
3. a1: k1+k2
4. a2: k1+k2
5. InjCase(a1; i. i, k1+i) = InjCase(a2; i. i, k1+i) (k1+k2)

a1 = a2

By: Analyze 4 THEN Analyze 3 THEN Reduce -1 THEN Analyze

Generated subgoals:

None

About: