Add tactic tn12.
Change notation for definitional equality from = to == or ≡
and use = for path connectedness.