proposition: Lemma lift_match_if_sumbool_ByteAlign {T1} {T3 : T1 -> Type} {P : forall t1 (t3 : T3 t1), Prop} {T2 T4 A : T1 -> Type} {B B' C} : forall (t1 : T1) (t3 : T3 t1) (b : forall t1 t3, {P t1 t3} + {~P t1 t3}) (t : _ -> option (A t1 * B * C)) (e : _ -> option (A t1 * B * C)) (b' : forall t1 t3, T2 t1 -> T4 t1 -> {P t1 t3} + {~P t1 t3}) (t' : forall t1 t3, T2 t1 -> T4 t1 -> _ -> option (A t1 * B' * C)) (e' : forall t1 t3, T2 t1 -> T4 t1 -> _ -> option (A t1 * B' * C)) (f : B' -> B) (t2 : T2 t1) (t4 : T4 t1), (b t1 t3 = b' t1 t3 t2 t4) -> (forall e'', t e'' = match t' t1 t3 t2 t4 e'' with | Some (a, b', c) => Some (a, f b', c) | None => None end) -> (forall e'', e e'' = match e' t1 t3 t2 t4 e'' with | Some (a, b', c) => Some (a, f b', c) | None => None end) -> (match b t1 t3 with left e'' => t e'' | right e'' => e e'' end) = match (fun t1 t2 t3 t4 => match b' t1 t3 t2 t4 with | left e'' => t' t1 t3 t2 t4 e'' | right e'' => e' t1 t3 t2 t4 e'' end) t1 t2 t3 t4 with | Some (a, b', c) => Some (a, f b', c) | None => None end.
proof: Proof. intros; destruct b; eauto; rewrite <- H; simpl; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word