exact_seq

Stream: condensed mathematics

[Johan Commelin]

A general remark about exact_seq. I've come to realise that it's often useful to prove lemmas about (f :: g :: L), where L is an arbitrary list of arrows. That way you can write things like (hL.drop 3).pair. It's slightly more efficient than using extract.