proposition: Lemma checktc6_all : forall c, tc6all c = true -> forall l p, validtc6 l -> valid63 p -> tc6i l c p = true.
proof: Proof. intros c; case c; [intros HH; discriminate | idtac]. intros p1 p2 p3 p4 p5 p6 Hc l p Hl; simpl in Hc; generalize Hc; clear Hc; case (validtc6_inv _ Hl). intros c1 (Hc1, [H2 | [H2 | [H2 | [H2 | [H2 | H2]]]]]); rewrite Hc1; rewrite H2; unfold tc6i; intros Ha Hp; match goal with |- int63i ?X _ = _ => apply (fun x => check63_all X x _ Hp); generalize Ha end; do 7 (case int63all; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik