proposition: Lemma Forall_proof_irrelevance {A P ls} (x y : @Forall A P ls) (pi : forall a (x y : P a), x = y) : x = y.
proof: Proof. rewrite <- (Forall_ForallT_Forall_eq x), <- (Forall_ForallT_Forall_eq y). apply f_equal. induction ls as [|v vs IHvs]. { reflexivity. } { unfold Forall_ForallT in *. revert IHvs. set (ls := v::vs). set (ls' := v::vs). set (ls'' := v::vs). pose (eq_refl : v::vs = ls) as H. pose (eq_refl : ls = ls') as H'. pose (eq_refl : ls = ls'') as H''. change (v::vs) with ls' in x. change (v::vs) with ls'' in y. change ((forall (x0 : Forall P (tl ls')) (y0 : Forall P (tl ls'')), proj1' (Forall_ForallT' (tl ls') (tl ls'') (f_equal (@tl _) H') (f_equal (@tl _) H'')) x0 = proj1' (Forall_ForallT' (tl ls'') (tl ls'') (f_equal (@tl _) H'') (f_equal (@tl _) H'')) y0) -> proj1' (Forall_ForallT' ls' ls'' H' H'') x = proj1' (Forall_ForallT' ls'' ls'' H'' H'') y). clearbody H H' H'' ls ls' ls''. intro IHvs. rewrite !step_Forall_ForallT'. simpl. destruct ls, x, y; try congruence. simpl in *. erewrite IHvs; clear IHvs. match goal with | [ |- match ?e with _ => _ end = match ?e' with _ => _ end ] => unify e e'; destruct e end. unfold eq_ind_r; simpl. repeat (f_equal; []). repeat match goal with | _ => intro | _ => progress simpl in * | _ => progress subst | _ => solve [ eauto with nocore ] | [ |- context[f_equal ?f ?H] ] => generalize (f_equal f H); clear H end. } 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