fact: Fixpoint Forall_tails_impl {T} (P P' : list T -> Type) (ls : list T) {struct ls} : Forall_tails (fun x => P x -> P' x) ls -> Forall_tails P ls -> Forall_tails P' ls := match ls return Forall_tails (fun x => P x -> P' x) ls -> Forall_tails P ls -> Forall_tails P' ls with | nil => fun H H' => H H' | x::xs => fun H H' => (fst H (fst H'), @Forall_tails_impl T P P' xs (snd H) (snd H')) end.
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