∀b,a:Top.  (fst([a / b]) ~ a)
{ (UnivCD THENA Auto) }
1. b : Top@i
2. a : Top@i
⊢ fst([a / b]) ~ a