proposition: Lemma impl_sum_match_match_option {A B ret s s' n r} {x : option A} (f : match x with | Some x' => s x' | None => n end -> ret) (g : s' r -> ret) : match match x return A + B with | Some x' => inl x' | None => inr r end with | inl x' => s x' | inr x' => s' x' end -> ret.
proof: Proof. destruct x; assumption. Defined.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.Lists.SetoidList Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Program.Program Coq.Classes.Morphisms Fiat.Common.Tactics.SplitInContext Fiat.Common.Tactics.Combinators Fiat.Common.Tactics.FreeIn Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.BreakMatch Fiat.Common.Tactics.Head Fiat.Common.Tactics.FoldIsTrue Fiat.Common.Tactics.SpecializeBy Fiat.Common.Tactics.DestructHyps Fiat.Common.Tactics.DestructSig Fiat.Common.Tactics.DestructHead Fiat.Common.Coq__8_4__8_5__Compat