proposition: Lemma aux1 : forall l p f, pathToPosAux (l ++ [Right]) f = Some p -> exists f', forall l', pathToPosAux (l ++ l') f = pathToPosAux l' f' /\ f' xH = p.
proof: Proof. induction l using list_ind'; intros. + simpl in *; inversion H; subst. exists f; intros. split; auto. + simpl in H; destruct a; inversion H. + pose proof IHl p; clear IHl. destruct a; destruct b; simpl in *. - pose proof (H0 (fun p0 => xO (f p0))); clear H0. apply H1 in H; clear H1. assumption. - pose proof (H0 (fun p0 => xI (f p0))); clear H0. apply H1 in H; clear H1. assumption. - inversion H. - inversion H. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets