proposition: Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) : nary_congruence_statement n k.
proof: Proof. have: k _ _ := _; rewrite {1}/k. elim: n k => [|n IHn] k k_P /= A; first exact: k_P. by apply: IHn => B e He; apply: k_P => f x1 x2 <-. Qed.
imports: Bool ssrmatching