Changes
1 changed files (+1/-1)
-
-
@@ -18,4 +18,4 @@ theorem A:(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l withexample:D (S l)∧l.Perm (S l):=by induction l with |nil=>grind |cons h t=>grind [A (n:=h)<|S t] |cons h t=>grind[A (n:=h)<|S t]
-