1. T : Type 2. a : T 3. a' : T 4. b : colist(T) 5. b' : colist(T) 6. [a / b] = [a' / b'] ∈ colist(T) 7. [a / b] = [a' / b'] ∈ {z:colist(T)| (z = [a / b] ∈ colist(T)) ∧ (z = [a' / b'] ∈ colist(T))} 8. b = b' ∈ colist(T) ⊢ b = b' ∈ colist(T)
BY { Auto }
Latex:
Latex:
1. T : Type
2. a : T
3. a' : T
4. b : colist(T)
5. b' : colist(T)
6. [a / b] = [a' / b']
7. [a / b] = [a' / b']
8. b = b'
\mvdash{} b = b'