namespace  http://mathhub.info/MitM/core/calculus 


import base http://mathhub.info/MitM/Foundation 
import arith http://mathhub.info/MitM/core/arithmetics 

theory FinSequences : base:?Logic =
	include ☞arith:?NaturalArithmetics 
	below : ℕ ⟶ type  = [n] ⟨ x : ℕ | ⊦ x < n ⟩ 
	toBelow : {n : ℕ} below (Succ n) # toB 1 
	succBelow : {n : ℕ} below n ⟶ below (Succ n) # succB 2

	belowIsSubtypeOfNat : {n : ℕ} (below n) <* ℕ 


	belowToNat : {n : ℕ} below (Succ n) ⟶ ℕ # btn 1 2
	belowToNatBaseCase : {m : ℕ} ⊦ belowToNat m (toBelow m) ≐ m
    belowToNatRecCase : {m : ℕ, b : below (Succ m)} ⊦ belowToNat (Succ m) (succBelow (Succ m) b) ≐ belowToNat m b 
  
    belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3
    belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 
	belwoToNatExample2_2 : ⊦ belowToNat (Succ 3) (succBelow (Succ 3) (toBelow 3)) ≐ 3
	
//	belowToNat2 : {n : ℕ} below (Succ  n) ⟶ ℕ ❘= [n, b] n ❘# btn2 %I1 ❙
//	belowToNat3 : {n : ℕ, m : ℕ} below n ⟶ ⊦ m < n ⟶ ℕ ❘= [n , m , b, p ] m ❘#  btn3 %I1 ❙
//	belowToNat4 : {n : ℕ} below n ⟶ ⟨ ℕ | [x] ⊦ x < n⟩ ❘# btn4 %I1❙


	finSeq : ℕ ⟶ type ⟶ type = [n , A] below n ⟶ A  

	
	nonEmptyFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool = [n, A , f] 0 < n # nefs %I1 %I2 
	
	disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool
	disjointFinSeq_prop_trivial :  {A : type,f : finSeq 0 A} ⊦ disjointFinSeq_prop 0 A f ≐ true
	disjointFinSeq_prop_step // : {A : type , n : ℕ , f : 
			finSeq (succ n) A} ⊦ disjointFinSeq_prop (succ n) A f ≐ ∀ [m1 : below (succ n)] ∀ [m2 : below (succ n)] ⊦ m1 ≠ m2 ⟶ ⊦ true 
	belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)
//	belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙ 
	
//	finSeqSum : {n : ℕ , b : below n} ❙