proposition: Lemma altACA A : @interchange (M A) (fun x y => x [~] y) (fun x y => x [~] y).
proof: Proof. move=> x y z t; rewrite !altA; congr (_ [~] _); by rewrite altAC. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)