proposition: Lemma prefixFreeCommutative : forall l1 l2, PrefixFree [l1;l2] -> PrefixFree [l2;l1].
proof: Proof. intros. inversion H. apply FreeCons. + apply FreeCons. - constructor. - intros. inversion H4. + intros. subst. eapply H3. - instantiate (1 := l2); left; auto. - inversion H4. * subst. inversion H4. subst. instantiate (1:= p1); instantiate (1 := p2). auto. * inversion H0. - inversion H0. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets