-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;
+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;