proposition: Lemma eq_rect_const {A x P} (u : P) {y} (H : x = y) : @eq_rect A x (fun _ => P) u y H = u.
proof: Proof. destruct H; 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