proposition: Lemma In_combine_sig {T P ls H x} (H' : In x ls) : In (exist P x (@Forall_forall1_transparent T P ls H _ H')) (combine_sig H).
proof: Proof. unfold combine_sig. induction ls; simpl in *; trivial. destruct_head or; subst; try first [ left; reflexivity ]. right. revert H. match goal with | [ |- context[@eq_refl ?A ?a] ] => generalize (@eq_refl A a) end. set (als := a::ls) in *. change als with (a::ls) at 1. clearbody als. intros e H. destruct H; [ exfalso; solve [ inversion e ] | ]. apply IHls. 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