You can think of GADTs as generating equalities when you match on a constructor. So when you open up `GIf(c, t, e)` you'll find c : vc expr' t : vt exp

You can think of GADTs as generating equalities when you match on a constructor. So when you open up `GIf(c, t, e)` you'll find c : vc expr' t : vt expr' e : ve expr' with an ambient type variable `a` and proofs of type equalities vc ~ bool vt ~ a ve ~ a When you solve those equations they'll work for any choices of `a` so long as `vt` and `ve` both can unify with it.