proposition: Lemma eq_Arr_eq : forall T (a b : T) (pf : a = b) (F G : T -> Type) val x, match pf in _ = x return F x -> G x with | eq_refl => val end x = match pf in _ = x return G x with | eq_refl => val match eq_sym pf in _ = x return F x with | eq_refl => x end end.
proof: Proof. destruct pf. reflexivity. Defined.