fact: Definition f_equal2_transparent {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : x1 = y1) : x2 = y2 -> f x1 x2 = f y1 y2 := match H in (_ = y) return (x2 = y2 -> f x1 x2 = f y y2) with | eq_refl => fun H0 : x2 = y2 => match H0 in (_ = y) return (f x1 x2 = f x1 y) with | eq_refl => eq_refl end end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations