proposition: Lemma nth'_map_property {A B B'} P Q (n : nat) (f g : A -> B) (f' : A -> list B') d ls (H' : forall v, (forall x, In x (f' v) -> Q x) -> f v = g v) (Hf : P (nth' n (map f ls) d)) (H : forall x, In x (nth' n (map f' ls) nil) -> Q x) : P (nth' n (map g ls) d).
proof: Proof. revert dependent n; induction ls as [|x xs IHxs]; intros. { simpl in *; assumption. } { destruct n as [|n]; simpl in *; rewrite nth'_nth in Hf |- *; simpl in *. { specialize (H' x). rewrite <- H'; [ assumption | ]. intro x'; specialize (H x'). rewrite nth'_nth in H; simpl in H. assumption. } { rewrite <- nth'_nth in Hf |- *. apply IHxs; clear IHxs; try assumption; []. intro x'; specialize (H x'). rewrite nth'_nth in H |- *; simpl in H. assumption. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts