-nlemma symmetric_foldrightlist2_aux :
-∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
- (∀x,y,z.f x y z = f y x z) →
- (∀acc:T2.∀l1,l2:list T1.
- ∀H1:(len_list T1 l1 = len_list T1 l2).
- ∀H2:(len_list T1 l2 = len_list T1 l1).
- (fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2)).
- #T1; #T2; #f; #H; #acc; #l1;
+nlemma symmetric_foldrightlist2_aux
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.
+ ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
+ (∀x,y,z.f x y z = f y x z) →
+ fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
+ #T1; #T2; #f; #acc; #l1;