proposition: Lemma ap_const {A B x y} (b : B) (p : x = y :> A) : f_equal (fun _ => b) p = eq_refl.
proof: Proof. case p; reflexivity. Defined.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common