Flow for Andrews-Curtis, including actors
HoTT cleanup - formal (dependent) function applications rewritten but old stuff not deleted.
a little further on functions
refining substitution target