proposition: Lemma step_Forall_ForallT' {A P ls ls' ls'' H' H''} : @Forall_ForallT' A P ls ls' ls'' H' H'' = @Forall_ForallT_step (@Forall_ForallT') A P ls ls' ls'' H' H''.
proof: Proof. destruct ls; reflexivity. Defined.
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