proposition: Lemma trunc_sym : forall (v : list A) (i j : nat), trunc (trunc v i) j = trunc (trunc v j) i.
proof: Proof. simple induction v. simpl in |- *. trivial with arith. simple induction i; simple induction j. trivial with arith. repeat rewrite trunc_O. simpl in |- *. trivial with arith. repeat rewrite trunc_O. simpl in |- *. trivial with arith. intros. simpl in |- *. rewrite H. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl