proposition: Lemma eq_option_eq : forall T (a b : T) (pf : a = b) (F : _ -> Type) val, match pf in _ = x return option (F x) with | eq_refl => val end = match val with | None => None | Some val => Some match pf in _ = x return F x with | eq_refl => val end end.
proof: Proof. destruct pf. destruct val; reflexivity. Defined.
imports: Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms ExtLib.Core.RelDec ExtLib.Structures.Reducible ExtLib.Structures.Traversable ExtLib.Structures.Applicative ExtLib.Structures.Functor ExtLib.Structures.FunctorLaws ExtLib.Data.Fun ExtLib.Tactics.Injection ExtLib.Tactics.Consider