proposition: Lemma matrix_4_ind : forall (P:(matrix 4) -> Type), forall (H:forall x_0_0 x_0_1 x_0_2 x_0_3 x_0_4, forall x_1_0 x_1_1 x_1_2 x_1_3 x_1_4, forall x_2_0 x_2_1 x_2_2 x_2_3 x_2_4, forall x_3_0 x_3_1 x_3_2 x_3_3 x_3_4, forall x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, P (x_0_0, ((x_0_1,(x_0_2,(x_0_3,x_0_4))), ((x_1_0,(x_2_0,(x_3_0,x_4_0))), (x_1_1, ((x_1_2,(x_1_3,x_1_4)), ((x_2_1,(x_3_1,x_4_1)), (x_2_2, ((x_2_3,x_2_4), ((x_3_2,x_4_2),(x_3_3,(x_3_4,(x_4_3,x_4_4)))))))) ))))), forall (m:matrix 4), P m.
proof: Proof. intros . refine match m with | (_, ((_,(_,(_,_))), ((_,(_,(_,_))), (_, ((_,(_,_)),((_,(_,_)),(_,((_,_),((_,_),(_,(_,(_,_)))))))))) )) => _ end. apply H. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)